Formal Set Topos

The purpose of this work is to clarify all topos definitions and variants of its components. Not much effort was put into providing all the examples, but one example, a topos on category of sets, is constructively presented in the finale.

As this cricial example definition is used in presheaf definition, the construction of category of sets is a mandatory excercise for any constructive topos library. We propose here cubical version of consctructive version of elementary topos on category of sets to demonstrate categorical semantics (from logic perspective) of the fundamental notion of set theory in mathematics.

Other disputed foundations for set theory could be taken as: ZFC, NBG, ETCS. We will disctinct syntetically: i) category theory; ii) set theory in univalent foundations; iii) topos theory, grothendieck topos, elementary topos.

This article provides a minimal self contained setup for topos on category of sets instance in cubicaltt. As for base library this is a chance to unvail the simplicity for the domain of intersection of: category theory, set theory, and topos theory.

One can admit two topos theory lineages. One lineage takes its roots from initial work on sheaves and specral sequences published by Jean Leray in 1945. Later this lineage was developed by Henri Paul Cartan and André Weil. The peak of lineage was settled with works of Jean-Pierre Serre, Alexander Grothendieck, and Roger Godement.

Second remarkable lineage take its root from William Lawvere and Myles Tierney. The main contribution is the reformulation of Grothendieck topology using subobject classifier. $$\def\mapright#1{\xrightarrow{{#1}}}\def\mapleft#1{\xleftarrow{{#1}}}\def\mapdown#1{\Big\downarrow\rlap{\raise2pt{\scriptstyle{#1}}}}\def\mapdiagl#1{\vcenter{\searrow}\rlap{\raise2pt{\scriptstyle{#1}}}}\def\mapdiagr#1{\vcenter{\swarrow}\rlap{\raise2pt{\scriptstyle{#1}}}}$$

Category Theory

First of all, a very simple category theory up to pullbacks is provided. We provide here all definitions only to keep the context valid.

Definition (Category Signature). The signature of category is a $\sum_{A:U}A \rightarrow A \rightarrow U$ where $U$ could be any universe. The $\mathrm{pr}_1$ projection is called $\mathrm{Ob}$ and $\mathrm{pr}_2$ projection is called $\mathrm{Hom}(a,b)$, where $a,b:\mathrm{Ob}$.

Precategory $\mathrm{C}$ defined as set of $\mathrm{Hom}_C(a,b)$ where $a,b:\mathrm{Ob}_C$ are objects defined by its $\mathrm{id}$ arrows $\mathrm{Hom}_C(x,x)$. Properfies of left and right units included with composition and its associativity.

Definition (Precategory). More formally, precategory $\mathrm{C}$ consists of the following. (i) A type $\mathrm{Ob}_C$, whose elements are called objects; (ii) for each $a,b: \mathrm{Ob}_C$, a set $\mathrm{Hom}_C(a,b)$, whose elements are called arrows or morphisms. (iii) For each $a: \mathrm{Ob}_C$, a morphism $1_a : \mathrm{Hom}_C(a,a)$, called the identity morphism. (iv) For each $a,b,c: \mathrm{Ob}_C$, a function $\mathrm{Hom}_C(b,c) \rightarrow \mathrm{Hom}_C(a,b) \rightarrow \mathrm{Hom}_C(a,c)$ called composition, and denoted $g \circ f$. (v) For each $a,b: \mathrm{Ob}_C$ and $f: \mathrm{Hom}_C(a,b)$, $f = 1_b \circ f$ and $f = f \circ 1_a$. (vi) For each $a,b,c,d: A$ and $f: \mathrm{Hom}_C(a,b)$, $g: \mathrm{Hom}_C(b,c)$, $h: \mathrm{Hom}_C(c,d)$, $h \circ (g \circ f ) = (h \circ g) \circ f$.

Definition (Terminal Object). Is such object $\mathrm{Ob}_C$, that $\Pi_{x,y:\mathrm{Ob}_C} \mathrm{isContr}(\mathrm{Hom}_C(y,x))$.

Definition (Categorical Pullback). The pullback of the cospan $A \mapright{f} C \mapleft{g} B$ is a object $A \times_{C} B$ with morphisms $pb_1 : \times_C \rightarrow A $, $pb_2 : \times_C \rightarrow B$, such that diagram commutes: $$ \begin{array}{ccc} A \times_{C} B & \mapright{\mathbf{pb_2}} & B \\ \mapdown{\mathbf{pb_1}} & \square & \mapdown{\mathbf{g}} \\ A & \mapright{\mathbf{f}} & C \\ \end{array}. $$ Pullback $(\times_C,pb_1,pb_2)$ must be universal, meaning that for any $(D,q_1,q_2)$ for which diagram also commutes there must exist a unique $u: D \rightarrow \times_C$, such that $pb_1 \circ u = q_1$ and $pb_2 \circ q_2$.

Set Theory

Here is the $\infty$-groupoid model of sets.

Definition (Mere proposition, $\mathrm{PROP}$). A type P is a mere proposition if for all $x,y: P$ we have $x=y$: $$ \mathrm{isProp}(P) = \prod_{x,y:P}(x=y). $$

Definition (0-type). A type A is a 0-type is for all $x,y: A$ and $p,q: x =_A y$ we have $p = q$.

Definition (1-type). A type A is a 1-type if for all $x,y: A$ and $p,q: x =_A y$ and $r,s:p =_{=_A} q$, we have $r = s$.

Definition (A set of elements, $\mathrm{SET}$). A type A is a $\mathrm{SET}$ if for all $x,y: A$ and $p,q: x = y$, we have $p = q$: $$ \mathrm{isSet}(A) = \prod_{x,y:A}\prod_{p,q:x=y}(p=q). $$

Theorem. If A is a set then A is a 1-type.

Theorem ($\Pi$-Contractability). if fiber is set then path space between any sections is contractible.

Theorem ($\Sigma$-Contractability). if fiber is set then $\Sigma$ is set.

Definition (Unit type, $1$). The unit $1$ is a type with one element.

Theorem ($1$ is a proposition).

Theorem ($1$ is a set).

Theorem (Category of Sets, $\mathrm{Set}$). Sets forms a Category. All compositional theorems are proved using reflection rule of internal language. The proof that $\mathrm{Hom}$ forms a set is taken through $\Pi$-contractability.

Topos Theory

Topos theory extends category theory with notion of topological structure reformulated in a categorical way as a category of sheaves on a site or as one that has cartesian closure and subobject classifier. We provide two definitions here.

Topological Structure

Definition (Topology). The topological structure on $\mathrm{A}$ (or topology) is a subset $S \in \mathrm{A}$ with following properties: i) any finite union of subsets of $\mathrm{S}$ belongs to $\mathrm{S}$; ii) any finite intersection of subsets of $\mathrm{S}$ belongs to $\mathrm{S}$. Subets of $\mathrm{S}$ are called open sets of family $\mathrm{S}$.

Here is a code snippet in Coq for this classical definition.

For fully functional general topology theorems and Zorn lemma you can refer to the Coq library topology by Daniel Schepler.

Grothendieck Topos

Grothendieck Topology is a calculus of coverings which generalizes the algebra of open covers of a topological space, and can exist on much more general categories. There are three variants of Grothendieck topology definition: i) sieves; ii) coverage; iii) covering failies. A category that has one of these three is called a Grothendieck site.

Examples: Zariski, flat, étale, Nisnevich topologies.

A sheaf is a presheaf (functor from opposite category to category of sets) which satisties patching conditions arising from Grothendieck topology, and applying the associated sheaf functor to preashef forces compliance with these conditions.

The notion of Grothendieck topos is a geometric flavour of topos theory, where topos is defined as category of sheaves on a Grothendieck site with geometric moriphisms as adjoint pairs of functors between topoi, that satisfy exactness properties.

As this flavour of topos theory uses category of sets as a prerequisite, the formal construction of set topos is cricual in doing sheaf topos theory.

Definition (Sieves). Sieves are a family of subfunctors $$\def\mapright#1{\xrightarrow{{#1}}} \def\mapdown#1{\Big\downarrow\rlap{\raise2pt{\scriptstyle{#1}}}} \def\mapdiagl#1{\vcenter{\searrow}\rlap{\raise2pt{\scriptstyle{#1}}}} \def\mapdiagr#1{\vcenter{\swarrow}\rlap{\raise2pt{\scriptstyle{#1}}}} R \subset Hom_C(\_,U), U \in \mathrm{C}, $$ such that following axioms hold: i) (base change) If $R \subset Hom_C(\_,U)$ is covering and $\phi : V \rightarrow U$ is a morphism of $\mathrm{C}$, then the subfuntor $$ \phi^{-1}(R) = \{ \gamma : W \rightarrow V\ |\ \phi \cdot \gamma \in R \} $$ is covering for $V$; ii) (local character) Suppose that $R,R' \subset Hom_C(\_,U)$ are subfunctors and R is covering. If $\phi^{-1}(R')$ is covering for all $\phi : V \rightarrow U$ in $R$, then $R'$ is covering; iii) $Hom_C(\_,U)$ is covering for all $U \in \mathrm{C}$.

Definition (Coverage). A coverage is a function assigning to each $\mathrm{Ob}_C$ the family of morphisms $\{f_i : U_i \rightarrow U \}_{i\in I}$ called covering families, such that for any $g: V \rightarrow U$ exist a covering family $\{h:V_j \rightarrow V\}_{j \in J}$ such that each composite $h_j \circ g$ factors some $f_i$: $$ \begin{array}{ccc} V_j & \mapright{k} & U_i \\ \mapdown{h} & \square & \mapdown{f_i} \\ V & \mapright{g} & U \\ \end{array} $$

Definition (Grothendieck Topology). Suppose category $\mathrm{C}$ has all pullbacks. Since $\mathrm{C}$ is small, a pretopology on $\mathrm{C}$ consists of families of sets of morphisms $$ \{ \phi_\alpha : U_\alpha \rightarrow U \}, U \in \mathrm{C}, $$ called covering families, such that following axioms hold: i) suppose that $\phi_\alpha : U_\alpha \rightarrow U$ is a covering family and that $\psi : V \rightarrow U$ is a morphism of $\mathrm{C}$. Then the collection $V \times_U U_\alpha \rightarrow V$ is a cvering family for $V$. ii) If $\{\phi_\alpha : U_\alpha \rightarrow U \}$ is covering, and $\{\gamma_{\alpha,\beta} : W_{\alpha,\beta} \rightarrow U_\alpha \}$ is covering for all $\alpha$, then the family of composites $$ W_{\alpha,\beta} \mapright{\gamma_{\alpha,\beta}} U_\alpha \mapright{\phi_\alpha} U. $$ is covering; iii) The family $\{1: U \rightarrow U\}$ is covering for all $U \in \mathrm{C}$.

Definition (Site). Site is a category having either a coverage, grothendieck topology, or sieves.

Definition (Presheaf). Presheaf of a category $\mathrm{C}$ is a functor from opposite category to category of sets: $\mathrm{C}^{op} \rightarrow \mathrm{Set}$.

Definition (Presheaf Category, $\mathrm{PSh}$). Presheaf category $\mathrm{PSh}$ for a site $\mathrm{C}$ is category were objects are presheaves and morphisms are natural transformations of presheaf functors.

Definition (Sheaf). Sheaf is a presheaf on a site. In other words a presheaf $F : \mathrm{C}^{op} \rightarrow \mathrm{Set}$ such that the cannonical map of inverse limit $$ F(U) \rightarrow \lim^{\leftarrow}_{V \to U \in R}{F(V)} $$ is an isomorphism for each covering sieve $R \subset Hom_C(\_,U)$. Equivalently, all induced functions $$ Hom_C(Hom_C(\_,U),F) \rightarrow Hom_C(R,F) $$ should be bijections.

Definition (Sheaf Category, $\mathrm{Sh}$). Sheaf category $\mathrm{Sh}$ is a category where objects are sheaves and morphisms are natural transformation of sheves. Sheaf category is a full subcategory of category of presheaves $\mathrm{PSh}$.

Definition (Grothendieck Topos). Topos is the category of sheaves $\mathrm{Sh}(\mathrm{C},J)$ on a site $\mathrm{C}$ with topology $J$.

Theorem (Giraud). A category $\mathrm{C}$ is a Grothiendieck topos if it has following properties: i) has all finite limits; ii) has small disjoint coproducts stable under pullbacks; iii) any epimorphism is coequalizer; iv) any equivalence relation $R \rightarrow E$ is a kernel pair and has a quotient; v) any coequalizer $R \rightarrow E \rightarrow Q$ is stably exact; vi) there is a set of objects that generates $\mathrm{C}$.

Definition (Geometric Morphism). Suppose that $\mathrm{C}$ and $\mathrm{D}$ are Grothendieck sites. A geometric morphism $$ f : \mathrm{Sh}(C) \rightarrow \mathrm{Sh}(D) $$ consists of functors $f_* : \mathrm{Sh}(C) \rightarrow \mathrm{Sh}(D)$ and $f^* : \mathrm{Sh}(D) \rightarrow \mathrm{Sh}(C)$ such that $f^*$ is left adjoint to $f_*$ and $f^*$ preserves finite limits. The left adjoint $f^*$ is called the inverse image functor, while $f_*$ is called the direct image. The inverse image functor $f^*$ is left and right exact in the sense that it preserves all finite colimits and limits, respectively.

Definition (Point of a Topos). A point $x$ of a topos $E$ is a geometric morphism: $p: \mathrm{Set} \rightarrow E$.

Definition (Stalk). The stalk at $x$ of an object $e \in E$ is the image of $e$ under corresponding inverse image morphism $x^{-1}: E \rightarrow \mathrm{Set}$.

Definition (Étale space $\mathrm{Spé}(F)$). Let $X$ — a topological space, $C$ a category and $F$ is a $C$-valued presheaf on $X$. Then, the étalé space is a a pair $(\mathrm{Ét}(F),\pi)$ where: i) $\mathrm{Ét}(F)$ is a disjoin union $\bigcup_{x\in X} F_x$ of stalks of $F$; ii) $\pi: \mathrm{Ét}(F) \rightarrow X$ is the canonical projection.

Elementary Topos

Giraud theorem was a synonymical topos definition that involved only topos properties but not site properties. That was a step forward in predicative definition. The other step was made by Lawvere and Tierney, by removing explicit dependance on categorical model of set theory (as category of set is used in definition of presheaf). This information was hidden into subobject classifier which was well defined through categorical pullback and property of being cartesian closed (having lambda calculus as internal language).

Elementary topos doesn't involve 2-categorical modeling, so we can construct set topos without using functors and natural transformations (that we need in geometrical topos theory flavour). This flavour of topos theory is more suited for logic needs rather than for geometry, as its set properties are hidden under predicative pullback definition of subobject classifier rather than functorial notation of presheaf functor. So we can simplify proofs at the homotopy levels, not to lift everything to 2-categorical model.

Definition (Monomorphism). A morphism $f : Y \rightarrow Z $ is a monic or mono if for any object $X$ and every pair of parralel morphisms $g_1,g_2: X \rightarrow Y$ the $$ f \circ g_1 = f \circ g_2 \rightarrow g_1 = g_2. $$ More abstractly, f is mono if for any $X$ the $\mathrm{Hom}(X,\_)$ takes it to an injective function between hom sets $\mathrm{Hom}(X,Y) \rightarrow \mathrm{Hom}(X,Z)$.

Definition (Subobject Classifier). In category $\mathrm{C}$ with finite limits, a subobject classifier is a monomorphism $true: 1 \rightarrow \Omega$ out of terminal object $\mathrm{1}$, such that for any mono $U \rightarrow X$ there is a unique morphism $\chi_U : X \rightarrow \Omega$ and a pullback diagram: $$ \begin{array}{ccc} U & \mapright{k} & \mathrm{1} \\ \mapdown{} & \square & \mapdown{} \\ X & \mapright{\chi_U} & \Omega \\ \end{array} $$

Theorem (Category of Sets has Subobject Classifier).

Definition (Cartesian Closed Categories). The category $\mathrm{C}$ is called cartesian closed if exists all: i) terminals; ii) products; iii) exponentials. Note that this definition lacks beta and eta rules which could be found in embedding $\mathrm{MLTT}$.

Theorem (Category of Sets has Cartesian Closure). As you can see from exp and pro we internalize $\Pi$ and $\Sigma$ types as $\mathrm{SET}$ instances, the $\mathrm{isSet}$ predicates are provided with contractability. Exitense of terminals is proved by $\mathrm{propPi}$. The same technique you can find in $\mathrm{MLTT}$ embedding.

Note that rules of cartesian closure form a type theoretical language called lambda calculus.

Definition (Elementary Topos). Topos is a precategory which is cartesian closed and has subobject classifier.

Theorem (Topos Definitions). Any Grothendieck topos is an elementary topos too. The proof is sligthly based on results of Giraud theorem.

Theorem (Category of Sets forms a Topos). There is a cartesian closure and subobject classifier for a categoty of sets.

Literature

[70]. P.T. Johnstone. Topos Theory. 2014, [71]. R. Goldblatt. Topoi: The Categorial Analysis of Logic. 2014, [72]. J.F. Jardine. Local Homotopy Theory. 2015.

Issue VIII: Formal Topos on Category of Sets