# 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.

# 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.

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

Precategory

```
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)))
```

```
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
```

```
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
```

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 the

```
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
```

```
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
```

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

```
data unit = tt
unitRec (C: U) (x: C): unit -> C = split tt -> x
unitInd (C: unit -> U) (x: C tt): (z:unit) -> C z = split tt -> x
```

`propUnit : isProp unit`

`setUnit : isSet unit`

```
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 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

Here is a code snippet 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

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.

such that following axioms hold: i) (base change) If

is covering for

```
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)
```

called covering families, such that following axioms hold:
i) suppose that

is covering;
iii) The family

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

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

is an isomorphism for each covering sieve

should be bijections.

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

consists of functors

## 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.

More abstractly, f is mono if for any

```
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
```

```
subobjectClassifier (C: precategory): U
= (omega: carrier C)
* (end: terminal C)
* (trueHom: hom C end.1 omega)
* (chi: (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,chi 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) (chi V X j) k)
```

```
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
```

```
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 form a type theoretical language called lambda calculus.

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

```
internal
: Topos Set
= (cartesianClosure,hasSubobject)
```

# 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 |