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.

(Category Signature). The signature of category is a where could be any universe. The projection is called and projection is called , where .

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

Precategory defined as set of where are objects defined by its arrows . Properfies of left and right units included with composition 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)))

(Precategory). More formally, precategory consists of the following. (i) A type , whose elements are called objects; (ii) for each , a set , whose elements are called arrows or morphisms. (iii) For each , a morphism , called the identity morphism. (iv) For each , a function called composition, and denoted . (v) For each and , and . (vi) For each and , , , .

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

(Terminal Object). Is such object , that .

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

(Categorical Pullback). The pullback of the cospan is a object with morphisms , , such that diagram commutes:

Pullback must be universal, meaning that for any for which diagram also commutes there must exist a unique , such that and .

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 -groupoid model of sets.

(Mere proposition, ). A type P is a mere proposition if for all we have :

(0-type). A type A is a 0-type is for all and we have .

(1-type). A type A is a 1-type if for all and and , we have .

(A set of elements, ). A type A is a if for all and , we have :

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

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

(-Contractability). if fiber is set then 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

(-Contractability). if fiber is set then is set.

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

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

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

( is a proposition).

propUnit : isProp unit

( is a set).

setUnit : isSet unit

(Category of Sets, ). Sets forms a Category. All compositional theorems are proved using reflection rule of internal language. The proof that forms a set is taken through -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 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

(Topology). The topological structure on (or topology) is a subset with following properties: i) any finite union of subsets of belongs to ; ii) any finite intersection of subsets of belongs to . Subets of are called open sets of family .

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.

(Sieves). Sieves are a family of subfunctors

such that following axioms hold: i) (base change) If is covering and is a morphism of , then the subfuntor

is covering for ; ii) (local character) Suppose that are subfunctors and R is covering. If is covering for all in , then is covering; iii) is covering for all .

(Coverage). A coverage is a function assigning to each the family of morphisms called covering families, such that for any exist a covering family such that each composite factors some :

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)

(Grothendieck Topology). Suppose category has all pullbacks. Since is small, a pretopology on consists of families of sets of morphisms

called covering families, such that following axioms hold: i) suppose that is a covering family and that is a morphism of . Then the collection is a cvering family for . ii) If is covering, and is covering for all , then the family of composites

is covering; iii) The family is covering for all .

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

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

(Presheaf). Presheaf of a category is a functor from opposite category to category of sets: .

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

(Presheaf Category, ). Presheaf category for a site is category were objects are presheaves and morphisms are natural transformations of presheaf functors.

(Sheaf). Sheaf is a presheaf on a site. In other words a presheaf such that the cannonical map of inverse limit

is an isomorphism for each covering sieve . Equivalently, all induced functions

should be bijections.

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

(Sheaf Category, ). Sheaf category is a category where objects are sheaves and morphisms are natural transformation of sheves. Sheaf category is a full subcategory of category of presheaves .

(Grothendieck Topos). Topos is the category of sheaves on a site with topology .

(Giraud). A category 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 is a kernel pair and has a quotient; v) any coequalizer is stably exact; vi) there is a set of objects that generates .

(Geometric Morphism). Suppose that and are Grothendieck sites. A geometric morphism

consists of functors and such that is left adjoint to and preserves finite limits. The left adjoint is called the inverse image functor, while is called the direct image. The inverse image functor is left and right exact in the sense that it preserves all finite colimits and limits, respectively.

(Point of a Topos). A point of a topos is a geometric morphism: .

(Stalk). The stalk at of an object is the image of under corresponding inverse image morphism .

(Étale space $é$ ). Let a topological space, a category and is a -valued presheaf on . Then, the étalé space is a a pair $É$ where: i) $É$ is a disjoin union of stalks of ; ii) $É$ 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.

(Monomorphism). A morphism is a monic or mono if for any object and every pair of parralel morphisms the

More abstractly, f is mono if for any the takes it to an injective function between hom sets .

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

(Subobject Classifier). In category with finite limits, a subobject classifier is a monomorphism out of terminal object , such that for any mono there is a unique morphism and a pullback diagram:

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)

(Category of Sets has Subobject Classifier).

(Cartesian Closed Categories). The category 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 .

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

(Category of Sets has Cartesian Closure). As you can see from exp and pro we internalize and types as instances, the predicates are provided with contractability. Exitense of terminals is proved by . The same technique you can find in 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 form a type theoretical language called lambda calculus.

elementary Topos). Topos is a precategory which is cartesian closed and has subobject classifier.

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

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

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

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.