Synthetic topos theory

[001L] A universal property of \(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U)\)

The following observation is not directly used elsewhere but indicates that étale morphisms are the characteristic of topos theory and provides inspiration for the design of a type theory of toposes.

[001M] Definition

Let \(U\) be a universe. A category with \(U\)-étale morphisms \(C\) consists of the following data.

  • -A category \(C.\mathord {\textnormal {\textsf {Carrier}}}\) with \(U\)-small limits.
  • -A univalent morphism \(C.\mathord {\textnormal {\textsf {p}}}:C.\mathbb {A}_{\bullet }\rightarrow C.\mathbb {A}\) in \(C.\mathord {\textnormal {\textsf {Carrier}}}\) called the universal étale morphism. Pullbacks of \(C.\mathord {\textnormal {\textsf {p}}}\) are called étale morphisms. For an object \(x:C.\mathord {\textnormal {\textsf {Carrier}}}\), let \(\mathord {\textnormal {\textsf {Etale}}}(x)\) denote the full subcategory of \(C.\mathord {\textnormal {\textsf {Carrier}}}/x\) spanned by the étale morphisms with codomain \(x\).
  • -All the identity morphisms in \(C.\mathord {\textnormal {\textsf {Carrier}}}\) are étale, étale morphisms are closed under composition, and étale morphisms are closed under diagonal.
  • -For every object \(x:C.\mathord {\textnormal {\textsf {Carrier}}}\), the category \(\mathord {\textnormal {\textsf {Etale}}}(x)\) has \(U\)-small colimits preserved by the inclusion \(\mathord {\textnormal {\textsf {Etale}}}(x)\rightarrow C.\mathord {\textnormal {\textsf {Carrier}}}/x\).
  • -For every morphism \(f:x\rightarrow y\) in \(C.\mathord {\textnormal {\textsf {Carrier}}}\), the pullback functor \({f}^{*}:\mathord {\textnormal {\textsf {Etale}}}(y)\rightarrow \mathord {\textnormal {\textsf {Etale}}}(x)\) preserves \(U\)-small colimits.
  • -\(C.\mathord {\textnormal {\textsf {p}}}\) is exponentiable.
A morphism of categories with \(U\)-étale morphisms is a structure-preserving functor. Note that preservation of universal étale morphism is a proposition because of univalence.

[001N] Exercise

Let \(U\) be a universe. Then \(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U)\) is the initial category with \(U\)-étale morphisms, where the universal étale morphism in \(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U)\) is \(\mathord {\textnormal {\textsf {p}}}:\mathbb {A}_{\bullet }\rightarrow \mathbb {A}\) defined in [000K].