Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Stack Representation of Finitely Presented Heyting Pretoposes I

Lingyuan Ye

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.

Stack Representation of Finitely Presented Heyting Pretoposes I

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.
Paper Structure (10 sections, 31 theorems, 85 equations)

This paper contains 10 sections, 31 theorems, 85 equations.

Table of Contents

  1. Introduction
  2. Duality for Finite Pretoposes
  3. Finite Categories as Models
  4. Duality for Finite Pretoposes
  5. Geometric Surjection
  6. Open Functors and Duality of Finite Heyting Pretoposes
  7. Stack Representation
  8. The $(2,1)$-Site of Finite Kripke Frames
  9. Stack Representation of Heyting Pretoposes
  10. From Gros to Petit

Key Result

Lemma 2.2

For any pretopos $\mathcal{D}$, its category of models $\mathrm{Mod}(\mathcal{D})$ is closed under filtered colimits in $[\mathcal{D},\mathbf{Set}]$, thus in particular is Cauchy complete.

Theorems & Definitions (74)

  • Definition 2.1
  • Lemma 2.2
  • proof
  • Lemma 2.3
  • proof
  • Lemma 2.4
  • proof
  • Proposition 2.5
  • proof
  • Corollary 2.6
  • ...and 64 more