Stack Representation of Finitely Presented Heyting Pretoposes I
Logic
2024-02-21 v1 Category Theory
Abstract
This is the first of a series of papers on stack representation of finitely presented Heyting pretoposes. In this paper, we provide the first step by constructing a (2, 1)-site, which can be thought of as the site of finite Kripke frames, such that the (2,1)-category of finitely presented Heyting pretoposes contravariantly embeds into the (2,1)- topos of stacks on this (2, 1)-site. This provides an entry point to use categorical and higher sheaf-theoretic tools to study the properties of certain classes of intuitionistic first-order theories.
Keywords
Cite
@article{arxiv.2402.13099,
title = {Stack Representation of Finitely Presented Heyting Pretoposes I},
author = {Lingyuan Ye},
journal= {arXiv preprint arXiv:2402.13099},
year = {2024}
}