{- Topos Theory: - Category, Pullback, Mono, Epi, Set, subobjectClassifier, CCC; - setSig, setPi, SET, Path; - Topos, Set Topos. Copyright (c) Groupoid Infinity, 2014-2018 -} module topos where import cat import fun import pi import iso_sigma epi (P: precategory) (X Y: carrier P) (f: hom P X Y): U = (Z: carrier P) (g1 g2: hom P Y Z) -> Path (hom P X Z) (compose P X Y Z f g1) (compose P X Y Z f g2) -> Path (hom P Y Z) g1 g2 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 -- Lawvere Topos 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) 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)) 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 -- Beta, Eta rules, Either, CoCartesian, DepTypes ? cartesianClosed : 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)) hasSubobject : subobjectClassifier Set = undefined Topos (cat: precategory) : U = (cartesianClosed: isCCC cat) * subobjectClassifier cat internal : Topos Set = (cartesianClosed,hasSubobject) presheaf (C: precategory): U = catfunctor (opCat C) Set Co (C: precategory) (cod: carrier C) : U = (dom: carrier C) * (morphism: hom C dom cod) * unit Delta (C: precategory) (d: carrier C) : U = (index: U) * (family: index -> Co C d) * unit Coverage (C: precategory): U = (cod: carrier C) * (fam: Delta C cod) * (coverings: carrier C -> Delta C cod -> U) * (coverings cod fam) site (C: precategory): U = (C: precategory) * Coverage C sheaf (C: precategory): U = (S: site C) * presheaf S.1 --- http://www.ams.org/notices/200409/what-is-illusie.pdf