Formal Set Topos

Elementary Topos on Category of Sets

Abstract

This page gives you minimal single-file setup for Set Topos 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.

Disputed foundations for set theory could be taken as: ZFC, NBG, ETCS, Topos Theory. We will disctinct syntetically: i) category theory; ii) set theory in univalent foundations; iii) topos theory, grothendieck topos, elementary topos, category of topoi with geometric morphisms.

One can admit two topos theory lineages. One lineage takes its roots from published by Jean Leray in 1945 initial work on sheaves and specral sequences. Later this lineage was developed by Henri Paul Cartan, André Weil. The peak of lineage was settled with works by 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 by using sobobject classifier.

We give here only minimal set of definitions needed for instantiating elementary topos of category of sets. Also very brief examination of three ways of topological definition: i) classical definition of topology in terms of open sets; ii) Grothendieck topos; iii) Elementary topos.


Category Theory

Very simple category theory subset up to pullbacks is provided. We give here all definitions to keep context valid.

Definition (Category Signature). The signature of category is a $\Sigma_{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}$.

cat: U = (A: U) * (A -> A -> U)

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 c and its associativity.

isPrecategory (C: cat): U = (id: (x: C.1) -> C.2 x x) * (c: (x y z: C.1) -> C.2 x y -> C.2 y z -> C.2 x z) * (homSet: (x y: C.1) -> isSet (C.2 x y)) * (left: (x y: C.1) -> (f: C.2 x y) -> Path (C.2 x y) (c x x y (id x) f) f) * (right: (x y: C.1) -> (f: C.2 x y) -> Path (C.2 x y) (c x y y f (id y)) f) * ( (x y z w: C.1) -> (f: C.2 x y) -> (g: C.2 y z) -> (h: C.2 z w) -> Path (C.2 x w) (c x z w (c x y z f g) h) (c x y w f (c y z w g h)))

Definition (Precategory). More formal, 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$.

carrier (C: precategory) : U hom (C: precategory) (a b: carrier C) : U compose (C: precategory) (x y z: carrier C) (f: hom C x y) (g: hom C y z) : hom C x z

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

isTerminal (C: precategory) (y: carrier C): U = (x: carrier C) -> isContr (hom C x y) terminal (C: precategory): U = (y: carrier C) * isTerminal C y

Definition (Categorical Pullback).

homTo (C: precategory) (X: carrier C): U = (Y: carrier C) * hom C Y X cospan (C: precategory): U = (X: carrier C) * (_: homTo C X) * homTo C X hasCospanCone (C: precategory) (D: cospan C) (W: carrier C) : U = (f: hom C W D.2.1.1) * (g: hom C W D.2.2.1) * Path (hom C W D.1) (compose C W D.2.1.1 D.1 f D.2.1.2) (compose C W D.2.2.1 D.1 g D.2.2.2) cospanCone (C: precategory) (D: cospan C): U = (W: carrier C) * hasCospanCone C D W isCospanConeHom (C: precategory) (D: cospan C) (E1 E2: cospanCone C D) (h: hom C E1.1 E2.1) : U = (_ : Path (hom C E1.1 D.2.1.1) (compose C E1.1 E2.1 D.2.1.1 h E2.2.1) E1.2.1) * ( Path (hom C E1.1 D.2.2.1) (compose C E1.1 E2.1 D.2.2.1 h E2.2.2.1) E1.2.2.1) cospanConeHom (C: precategory) (D: cospan C) (E1 E2: cospanCone C D) : U = (h: hom C E1.1 E2.1) * isCospanConeHom C D E1 E2 h isPullback (C: precategory) (D: cospan C) (E: cospanCone C D) : U = (h: cospanCone C D) -> isContr (cospanConeHom C D h E) hasPullback (C: precategory) (D: cospan C) : U = (E: cospanCone C D) * isPullback C D E

Set Theory

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

Definition ($\mathrm{PROP}$). A 0-type is a mere proposition.

Definition ($\mathrm{SET}$). A 1-type is a set.

data N = Z | S (n: N) n_grpd (A: U) (n: N): U = (a b: A) -> rec A a b n where rec (A: U) (a b: A) : (k: N) -> U = split { Z -> Path A a b ; S n -> n_grpd (Path A a b) n } isContr (A: U): U = (x: A) * ((y: A) -> Path A x y) isProp (A: U): U = n_grpd A Z isSet (A: U): U = n_grpd A (S Z) PROP : U = (X:U) * isProp X SET : U = (X:U) * isSet X

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

setPi (A: U) (B: A -> U) (h: (x: A) -> isSet (B x)) (f g: Pi A B) (p q: Path (Pi A B) f g) : Path (Path (Pi A B) f g) p q

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

setSig (A:U) (B: A -> U) (sA: isSet A) (sB : (x:A) -> isSet (B x)) : isSet (Sigma A B)

Theorem ($1$ is a proposition).

propUnit : isProp unit

Theorem ($1$ is a set).

setUnit : isSet unit

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

Set: precategory = ((Ob,Hom),id,c,HomSet,L,R,Q) where Ob: U = SET Hom (A B: Ob): U = A.1 -> B.1 id (A: Ob): Hom A A = idfun A.1 c (A B C: Ob) (f: Hom A B) (g: Hom B C): Hom A C = o A.1 B.1 C.1 g f HomSet (A B: Ob): isSet (Hom A B) = setFun A.1 B.1 B.2 L (A B: Ob) (f: Hom A B): Path (Hom A B) (c A A B (id A) f) f = refl (Hom A B) f R (A B: Ob) (f: Hom A B): Path (Hom A B) (c A B B f (id B)) f = refl (Hom A B) f Q (A B C D: Ob) (f: Hom A B) (g: Hom B C) (h: Hom C D) : Path (Hom A D) (c A C D (c A B C f g) h) (c A B D f (c B C D g h)) = refl (Hom A D) (c A B D f (c B C D g h))

Topos Theory

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

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}$ is belong to $\mathrm{S}$; ii) any finite intersection of subsets of $\mathrm{S}$ is belong to $\mathrm{S}$. Subets of $\mathrm{S}$ are called open sets of family $\mathrm{S}$.

Here is given a code in Coq, for this classical definition.

Structure topology (A : Type) := { open :> (A -> Prop) -> Prop; empty_open: open (empty _); full_open: open (full _); inter_open: forall u, open u -> forall v, open v -> open (inter A u v) ; union_open: forall s, (subset _ s open) -> open (union A s) }.
Definition subset (A: Type) (u v : A -> Prop) := (forall x : A, u x -> v x). Definition disjoint (A: Type) (u v : A -> Prop) := forall x, ~ (u x /\ v x). Definition union (A: Type) (B :(A -> Prop) -> Prop) := fun x : A => exists U, B U /\ U x. Definition inter (A: Type) (u v : A -> Prop) := fun x : A => u x /\ v x. Definition empty (A: Type) := fun x : A => False. Definition full (A: Type) := fun x : A => True.

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

Grothendieck Topos

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$: $$ \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}}}} \begin{array}{ccc} V_j & \mapright{k} & U_i \\ \mapdown{} & \square & \mapdown{} \\ V & \mapright{g} & U \\ \end{array} $$

Co (C: precategory) (cod: carrier C) : U = (dom: carrier C) * (hom C dom cod) Delta (C: precategory) (d: carrier C) : U = (index: U) * (index -> Co C d) Coverage (C: precategory): U = (cod: carrier C) * (fam: Delta C cod) * (coverings: carrier C -> Delta C cod -> U) * (coverings cod fam)

Definition (Grothendieck Topology).

Definition (Site). Site is a category having a coverage.

site (C: precategory): U = (C: precategory) * Coverage C

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

presheaf (C: precategory): U = catfunctor (opCat C) Set

Definition (Sheaf, $\mathrm{Sh}$). Sheaf $\mathrm{Sh}$ is a presheaf on a site.

sheaf (C: precategory): U = (S: site C) * presheaf S.1

Definition (Grothendieck Topos). A category $\mathrm{C}$ is called Grothendieck Topos if exists a site such that category of sheaves on $\mathrm{C}$ equals $\mathrm{C}$ or $\mathrm{Sh}(\mathrm{C},J)=\mathrm{C}$. In other words a topos is the category of sheaves $\mathrm{Sh}(\mathrm{C},J)$ on a site.

Definition (Geometric Morphism). A morphism between Grothendieck topoi.

Elementary Topos

Definition (Monomorphism).

mono (P: precategory) (Y Z: carrier P) (f: hom P Y Z): U = (X: carrier P) (g1 g2: hom P X Y) -> Path (hom P X Z) (compose P X Y Z g1 f) (compose P X Y Z g2 f) -> Path (hom P X Y) g1 g2

Definition (Subobject Classifier).

subobjectClassifier (C: precategory): U = (omega: carrier C) * (end: terminal C) * (trueHom: hom C end.1 omega) * (xi: (V X: carrier C) (j: hom C V X) -> hom C X omega) * (square: (V X: carrier C) (j: hom C V X) -> mono C V X j -> hasPullback C (omega,(end.1,trueHom),(X,xi V X j))) * ((V X: carrier C) (j: hom C V X) (k: hom C X omega) -> mono C V X j -> hasPullback C (omega,(end.1,trueHom),(X,k)) -> Path (hom C X omega) (xi V X j) k)

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}$.

isCCC (C: precategory): U = (Exp: (A B: carrier C) -> carrier C) * (Prod: (A B: carrier C) -> carrier C) * (Apply: (A B: carrier C) -> hom C (Prod (Exp A B) A) B) * (P1: (A B: carrier C) -> hom C (Prod A B) A) * (P2: (A B: carrier C) -> hom C (Prod A B) B) * (Term: terminal C) * unit

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.

cartesianClosure : isCCC Set = (expo,prod,appli,proj1,proj2,term,tt) where exp (A B: SET): SET = (A.1 -> B.1, setFun A.1 B.1 B.2) pro (A B: SET): SET = (prod A.1 B.1, setSig A.1 (\(_ : A.1) -> B.1) A.2 (\(_ : A.1) -> B.2)) expo: (A B: SET) -> SET = \(A B: SET) -> exp A B prod: (A B: SET) -> SET = \(A B: SET) -> pro A B appli: (A B: SET) -> hom Set (pro (exp A B) A) B = \(A B:SET)-> \(x:(pro(exp A B)A).1)-> x.1 x.2 proj1: (A B: SET) -> hom Set (pro A B) A = \(A B: SET) (x: (pro A B).1) -> x.1 proj2: (A B: SET) -> hom Set (pro A B) B = \(A B: SET) (x: (pro A B).1) -> x.2 unitContr (x: SET) (f: x.1 -> unit) : isContr (x.1 -> unit) = (f, \(z: x.1 -> unit) -> propPi x.1 (\(_:x.1)->unit) (\(x:x.1) ->propUnit) f z) term: terminal Set = ((unit,setUnit),\(x: SET) -> unitContr x (\(z: x.1) -> tt))

Note that rules of cartesian closure forms a type theoretical langage called lambda calculus.

Definition (Elementary Topos). Topos.

Topos (cat: precategory) : U = (cartesianClosure: isCCC cat) * subobjectClassifier cat

Theorem (Category of Sets forms a Topos).

internal : Topos Set = (cartesianClosure,hasSubobject)