{- Iso Type: - Commutative Square - Iso To Path Copyright (c) Groupoid Infinity, 2014-2018. -} module iso where import retract import equiv import set -- u -- a ------> b -- | | -- p | | q -- | | -- V V -- c ------> d -- v Square (A: U)(a b c d: A)(u: Path A a b)(v: Path A c d)(p: Path A a c)(q: Path A b d): U = PathP ( (PathP ( A) (u @ i) (v @ i))) p q constSquare (A: U) (a: A) (p: Path A a a): Square A a a a a p p p p = comp (<_> A) a [ (i = 0) -> p @ j \/ - k, (i = 1) -> p @ j /\ k, (j = 0) -> p @ i \/ - k, (j = 1) -> p @ i /\ k ] isIso (A B: U): U = (f: A -> B) * (g: B -> A) * (s: section A B f g) * ( retract A B f g) ISO: U = (A: U) * (B: U) * isIso A B lemIso (A B: U) (f: A -> B) (g: B -> A) (s: section A B f g) (t: retract A B f g) (y: B) (x0 x1: A) (p0: Path B y (f x0)) (p1: Path B y (f x1)) : Path (fiber A B f y) (x0,p0) (x1,p1) = (p @ i,sq1 @ i) where rem0: Path A (g y) x0 = comp ( A) (g (p0 @ i)) [ (i = 1) -> t x0, (i = 0) -> g y ] rem1: Path A (g y) x1 = comp ( A) (g (p1 @ i)) [ (i = 1) -> t x1, (i = 0) -> g y ] p: Path A x0 x1 = comp ( A) (g y) [ (i = 0) -> rem0, (i = 1) -> rem1 ] fill0: Square A (g y)(g (f x0)) (g y) x0 ( g (p0 @ i)) rem0 ( g y) (t x0) = comp ( A) (g (p0 @ i)) [ (i = 1) -> t x0 @ j /\ k, (i = 0) -> g y, (j = 0) -> g (p0 @ i) ] fill1: Square A(g y)(g(f x1))(g y) x1 (g (p1@i)) rem1 ( g y) (t x1) = comp ( A) (g (p1 @ i)) [ (i = 1) -> t x1 @ j /\ k, (i = 0) -> g y, (j = 0) -> g (p1 @ i) ] fill2: Square A (g y) (g y) x0 x1 ( g y) p rem0 rem1 = comp ( A) (g y) [ (i = 0) -> rem0 @ j /\ k, (i = 1) -> rem1 @ j /\ k, (j = 0) -> g y ] sq: Square A(g y)(g y)(g(f x0))(g(f x1))(g y) (g (f(p@i)))(g(p0@j))(g(p1@j)) = comp ( A) (fill2 @ i @ j) [ (i = 0) -> fill0 @ j @ -k, (i = 1) -> fill1 @ j @ -k, (j = 0) -> g y, (j = 1) -> t (p @ i) @ -k ] sq1: Square B y y (f x0) (f x1) (y) ( f (p @ i)) p0 p1 = comp ( B) (f (sq @ i @j)) [ (i = 0) -> s (p0 @ j), (i = 1) -> s (p1 @ j), (j = 1) -> s (f (p @ i)), (j = 0) -> s y ] isoToEquiv (A B: U) (f: A -> B) (g: B -> A) (s: section A B f g) (t: retract A B f g): isEquiv A B f = \(y:B) -> ((g y,s y@-i),\ (z:fiber A B f y) -> lemIso A B f g s t y (g y) z.1 (s y@-i) z.2) equivProp (A B: U) (a: isProp A) (b: isProp B) (f: A -> B) (g: B -> A): equiv A B = (f, isoToEquiv A B f g (\(y:B)->b(f(g y))y) (\(x:A)->a(g(f x))x)) -- pi version of isoPath isoPath (A B: U) (f: A -> B) (g: B -> A) (s: section A B f g) (t: retract A B f g): Path U A B = Glue B [ (i = 0) -> (A,f,isoToEquiv A B f g s t), (i = 1) -> (B,idfun B,idIsEquiv B) ] testIsoPath (A B : U) (f : A -> B) (g : B -> A) (s : (y : B) -> Path B (f (g y)) y) (t : (x : A) -> Path A (g (f x)) x) (a:A) : Path B (f a) (trans A B (isoPath A B f g s t) a) = comp (<_>B) (comp (<_>B) (f a) [(i=0) -> <_> f a]) [(i=0) -> <_> f a] -- sigma version of isoPath isoToPath (i: ISO): Path U i.1 i.2.1 = isoPath i.1 i.2.1 i.2.2.1 i.2.2.2.1 i.2.2.2.2.1 i.2.2.2.2.2 -- A proof that two propositions with maps between them can be identified with each other propPath (A B: U) (f: A -> B) (g: B -> A) (pa: isProp A) (pb: isProp B): Path U A B = isoToPath (A,B,f,g,(\ (b: B) -> pb (f (g b)) b),(\ (a: A) -> pa (g (f a)) a)) iso_Form (A B: U) : U = isIso A B -> Path U A B iso_Intro (A B: U) : iso_Form A B = \(x: isIso A B) -> isoToPath (A,B,x) iso_Elim (A B: U) : Path U A B -> isIso A B = \(p: Path U A B) -> (coerce A B p,coerce B A (p@-i), x p,y p) where x (p: Path U A B): section A B (coerce A B p) (coerce B A (p@-i)) = undefined y (p: Path U A B): retract A B (coerce A B p) (coerce B A (p@-i)) = undefined iso_Comp (A B : U) (p : Path U A B) : Path (Path U A B) (iso_Intro A B (iso_Elim A B p)) p = undefined iso_Uniq (A B : U) (p: isIso A B) : Path (isIso A B) (iso_Elim A B (iso_Intro A B p)) p = undefined IsoPathType (A B: U): isIso (isIso A B) (Path U A B) = (iso_Intro A B,iso_Elim A B,iso_Comp A B,iso_Uniq A B) PiType (A: U) (B: A -> U): isIso (Pi A B) (Pi A B) = (app A B,app A B,Pi_Eta A B,Pi_Eta A B) UnivType (A B: U): isIso (equiv A B) (Path U A B) = (equivToPath A B, pathToEquiv A B,eqToEq A B,idToPath A B)