{- Univalence: - univ. Copyright (c) Groupoid Infinity, 2014-2018. -} module univ where import retract import equiv import sigma import path import iso {- Univalence theorems are isomorphic at any level of equality: univalence (B: U): isContr ((A: U) * equiv B A) = undefined 1. Path (A = B) - path 2. Equiv (A ~ B) - sigma, fibrant 3. Iso (A == B) - adjoints Path: built-in Equiv: isContr (A: U): U = (x: A) * ((y: A) -> Path A x y) fiber (A B: U) (f: A -> B) (y: B): U = (x: A) * Path B y (f x) isEquiv (A B: U) (f: A -> B): U = (y: B) -> isContr (fiber A B f y) Iso: isIso (A B: U): U = (f: A -> B) * (g: B -> A) * (s: section A B f g) * (t: retract A B f g) * unit Iso(Equiv,Path) -- equivToPath, pathToEquiv Equiv(swap(Equiv),Iso(Equ,Equiv)) -- univalence, (slow) Equiv(Equiv,Iso(Path,Equiv)) -- univalence, (fast) Path(Path,Equiv) -- pathEqEquiv Equiv(Path,Equiv) -- pathEquivEquiv -} -- This is Corollary 10 of the cubical type theory paper -- (the proof of theorem 9 is inlined) (due to Fabian Ruch). univalenceAlt (B: U): isContr ((A: U) * equiv A B) = ((B,idEquiv B), \(w: (X:U) * equiv X B) -> let GlueB: U = Glue B [(i=0) -> (B,idEquiv B), (i=1) -> w] unglueB (g: GlueB): B = unglue g [(i=0) -> (B,idEquiv B),(i=1) -> w] in (GlueB,unglueB, \(b: B) -> ((glue (comp ( B) b [(i=0) -> b,(i=1) -> (w.2.2 b).1.2]) [(i=0) -> b, (i=1) -> (w.2.2 b).1.1] , fill ( B) b [(i=0) -> b, (i=1) -> (w.2.2 b).1.2]), \(v: fiber GlueB B unglueB b) -> (glue (comp ( B) b [(i=0) -> v.2 @ (j /\ k), (i=1) -> ((w.2.2 b).2 v @ j).2, (j=0) -> fill ( B) b [(i=0) -> b, (i=1) -> (w.2.2 b).1.2], (j=1) -> v.2]) [(i=0)-> v.2 @ j,(i=1) -> ((w.2.2 b).2 v @ j).1], fill ( B) b [(i=0) -> v.2 @ (j /\ l), (i=1) -> ((w.2.2 b).2 v @ j).2, (j=0) -> fill ( B) b [(i=0) -> b, (i=1) -> (w.2.2 b).1.2], (j=1) -> v.2])))) -- A version univalence. This is Corollary 11 of the cubical type theory paper. thmUniv (t: (A X: U) -> Path U X A -> equiv X A) (A: U) : (X: U) -> isEquiv (Path U X A) (equiv X A) (t A X) = equivFunFib U (\(X : U) -> Path U X A) (\(X: U) -> equiv X A) (t A) (isContrSingl' U A) (univalenceAlt A) univalence (A X: U) : isEquiv (Path U X A) (equiv X A) (transEquiv' A X) = thmUniv transEquiv' A X -- Univalence Intro ua (A B: U) (e: equiv A B): Path U A B = Glue B [ (i = 0) -> (A,e), (i = 1) -> (B,idEquiv B) ] uabeta (A B: U) (e: equiv A B): Path (A -> B) (trans A B (ua A B e)) e.1 = \(a: A) -> fill (<_> B) (fill (<_> B) (e.1 a) [] @ -i) [] @ -i uabetaTransEquiv (A B: U) (e: equiv A B) : Path (A -> B) (transEquiv A B (ua A B e)).1 e.1 = \(a: A) -> (uabeta A B e @ i) (fill (<_> A) a [] @ -i) uaret (A B: U): retract (equiv A B) (Path U A B) (ua A B) (transEquiv A B) = \(e: equiv A B) -> equivLemma A B (transEquiv A B (ua A B e)) e (uabetaTransEquiv A B e) f1 (A: U) (p: (B: U) * equiv A B): singl U A = (p.1,ua A p.1 p.2) f2 (A: U) (p: singl U A): ((B: U) * equiv A B) = (p.1,transEquiv A p.1 p.2) corrUniv (A B: U) : Path U (Path U A B) (equiv A B) = equivPath (Path U A B) (equiv A B) (transEquiv' B A) (univalence B A) corrUniv' (A B: U): equiv (Path U A B) (equiv A B) = (transEquiv' B A,univalence B A) -- Elimination principle for equivalences contrSinglEquiv (A B: U) (f: equiv A B): Path ((X: U) * equiv X B) (B,idEquiv B) (A,f) = isContrProp ((X: U) * equiv X B) (univalenceAlt B) (B,idEquiv B) (A,f) elimEquiv (B: U) (P: (A: U) -> (A -> B) -> U) (d: P B (idfun B)) (A: U) (f: equiv A B): P A f.1 = subst((X: U) * equiv X B) T (B,idEquiv B) (A,f) (contrSinglEquiv A B f) d where T (z:(X: U) * equiv X B): U = P z.1 z.2.1 -- Elimination principle for iso elimIso (B: U) (Q: (A: U) -> (A -> B) -> (B -> A) -> U) (h1: Q B (idfun B) (idfun B)) (A: U) (f: A -> B): (g: B -> A) -> section A B f g -> retract A B f g -> Q A f g = rem1 A f where P (A: U) (f: A -> B): U = (g: B -> A) -> section A B f g -> retract A B f g -> Q A f g rem: P B (idfun B) = \ (g: B -> B) (sg: section B B (idfun B) g) (rg: retract B B (idfun B) g) -> substInv (B -> B) (Q B (idfun B)) g (idfun B) ( \(b: B) -> (sg b) @ i) h1 rem1 (A: U) (f: A -> B): P A f = \(g: B -> A) (sg: section A B f g) (rg: retract A B f g) -> elimEquiv B P rem A (f,isoToEquiv A B f g sg rg) g sg rg elimIsIso (A : U) (Q : (B : U) -> (A -> B) -> (B -> A) -> U) (d : Q A (idfun A) (idfun A)) (B : U) (f : A -> B) (g : B -> A) (sg : section A B f g) (rg : retract A B f g) : Q B f g = elimIso A (\(B : U) (f : B -> A) (g : A -> B) -> Q B g f) d B g f rg sg ------------------------------------------ VERY SLOW {- uaretsig (A: U): retract ((B: U) * equiv A B) (singl U A) (f1 A) (f2 A) = \(p: (B: U) * equiv A B) -> (p.1,uaret A p.1 p.2 @ i) univalenceAlt' (B: U) : isContr ((A: U) * equiv B A) = retIsContr ((A:U) * equiv B A) (singl U B) (f1 B) (f2 B) (uaretsig B) (isContrPath B) thmUniv' (t: (A X: U) -> Path U A X -> equiv A X) (A: U) : (X: U) -> isEquiv (Path U A X) (equiv A X) (t A X) = equivFunFib U (\(X: U) -> Path U A X) (\(X: U) -> equiv A X) (t A) (isContrSingl U A) (univalenceAlt' A) univalence' (A X: U): isEquiv (Path U A X) (equiv A X) (transEquiv A X) = thmUniv' transEquiv A X -} -----------------