natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
Theories of presheaf type though being geometric theories of a particular “simple” and tractable type are yet ubiquitous in the sense that every geometric theory is a quotient theory? of some theory of presheaf type.
A geometric theory $\mathbb{T}$ is of presheaf type if its classifying topos $Set[\mathbb{T}]$ is equivalent to a presheaf topos.
Any cartesian theory $\mathbb{T}$ being (modulo neglectable size issues^{1}) classified by $Set^{\mathbb{T}-Mod_{fp}(Set)}$ is of presheaf type with $\mathbb{T}\text{-}Mod_{fp}(Set)$ the category of finitely presentable $\mathbb{T}$-models in $Set$.
More concretely, e.g. the theory of objects or the theory of intervals are of presheaf type being classified by the object classifier respectively by the topos of simplicial sets.
The inconsistent theory with axiom $\top\vdash\bot$ is of presheaf type since it is classified by the initial Grothendieck topos $\mathbf{1}\simeq Pr(\emptyset)$, the presheaf topos on the empty category.
For a category $\mathcal{M}$ the following are equivalent:
$\mathcal{M}$ is finitely accessible.
$\mathcal{M}\simeq Pts(Set^{\mathcal{C}})$ the category of points of some presheaf topos.
$\mathcal{M}\simeq \mathbb{T}\text{-}Mod(Set)$ for some theory $\mathbb{T}$ of presheaf type.
$\mathcal{M}\simeq Ind \text{-}\mathcal{C}$ for some small category $\mathcal{C}$.
Cf. Beke (2004, p.923) and the references given there. In fact, these equivalences are mostly (direct consequences of) classical results in the theory of accessible categories or Grothendieck toposes.
Note that despite the above equivalences the finite accessibility of $\mathbb{T}\text{-}Mod(Set)$ does not imply that $\mathbb{T}$ itself is of presheaf type! One sees this already in case $\mathbb{T}\text{-}Mod(Set)=\emptyset$ since there famously are non trivial (Boolean sheaf) toposes lacking points (“non empty generalized spaces without points”) yet up to Morita equivalence the only theory of presheaf type corresponding to the finite accessibility of the empty category is the inconsistent theory.
The following proposition shows in which sense theories of presheaf type are still determined by their (finitely presentable) models in $Set$:
A geometric theory $\mathbb{T}$ is of presheaf type iff (modulo neglectable size issues)
Proof. “$\Rightarrow$”:
(Cf. Caramello 2018, pp.198f)
By assumption $Set[\mathbb{T}]\simeq [\mathcal{C}, Set]$. Since $[\mathcal{C},Set]\simeq [\hat{\mathcal{C}}, Set]$ (by Johnstone 2002, p.10) we can assume that $\mathcal{C}$ is Cauchy complete.
We have:
$Ind\text{-}\mathcal{C}\simeq Flat(\mathcal{C}^{op}, Set)$ (by Johnstone 2002, p.723, or Caramello 2018, p.198)
$(Ind\text{-}\mathcal{C})_{fp}\simeq \mathcal{C}$ (by Johnstone 2002 4.2.2.(iii), p.724)
$\mathbb{T}\text{-}Mod(Set)\simeq Flat(\mathcal{C}^{op}, Set)$ (from Diaconescu’s theorem).
Whence $(Ind\text{-}\mathcal{C})_{fp}\simeq (\mathbb{T}\text{-}Mod (Set))_{fp} =\mathbb{T}\text{-}Mod_{fp}(Set)\simeq \mathcal{C}$ and, accordingly, $[\mathcal{C},Set]]\simeq [\mathbb{T}\text{-}Mod_{fp}(Set),Set]$. $\qed$
In other words, theories of presheaf type are precisely those geometric theories $\mathbb{T}$ such that their classifying toposes $Set[\mathbb{T}]$ can be represented as presheaf toposes $Set^{\mathbb{T}\text{-}Mod_{fp}(Set)}$.
This implies e.g. that any consistent theory of presheaf type has models in $Set$.
Tibor Beke, Theories of presheaf type , JSL 69 no.3 (2004) pp.923-934. (pdf)
Olivia Caramello, Theories, Sites, Toposes , Oxford UP 2018. (chapters 6-9)
Matthias Hutzler, Syntactic presentations for glued toposes and for crystalline toposes, Phd. diss. Universität Augsburg 2021. (arXiv:2206.11244)
Peter Johnstone, Sketches of an Elephant vols.1-2 , Oxford UP 2002.
This means here (and in the following) that the essentially small category $\mathbb{T}\text{-}Mod_{fp}(Set)$ has to be replaced by a skeleton. ↩
Last revised on April 23, 2023 at 18:25:14. See the history of this page for a list of all contributions to it.