From: Anders Mörtberg Date: Mon, 4 Jan 2016 18:44:13 +0000 (+0100) Subject: Cleaning and removal of duplicate code. Put all proofs of univalence in the same... X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=2bae4a685c7418bfff34257beb2231b2e47d8f95;p=cubicaltt.git Cleaning and removal of duplicate code. Put all proofs of univalence in the same file --- diff --git a/examples/equiv.ctt b/examples/equiv.ctt index fc15018..c617191 100644 --- a/examples/equiv.ctt +++ b/examples/equiv.ctt @@ -7,20 +7,6 @@ import prelude fiber (A B : U) (f : A -> B) (y : B) : U = (x : A) * Id B y (f x) -isContr (A:U) : U = (a:A) * ((x:A) -> Id A a x) - -propIsContr (A:U) (z0 z1:isContr A) : Id (isContr A) z0 z1 = - (p0 a1@j, - \ (x:A) -> - comp (<_>A) (lem1 x@i@j) [ (i=0) -> p0 a1@j, (i=1) -> p0 x@(j\/k), - (j=0) -> p0 x@(i/\k), (j=1) -> p1 x@i ]) - where - a0 : A = z0.1 - p0 : (x:A) -> Id A a0 x = z0.2 - a1 : A = z1.1 - p1 : (x:A) -> Id A a1 x = z1.2 - lem1 (x:A) : IdP (Id A a0 (p1 x@i)) (p0 a1) (p0 x) = p0 (p1 x@i) @ j - isEquiv (A B : U) (f : A -> B) : U = (y : B) -> isContr (fiber A B f y) equiv (A B : U) : U = (f : A -> B) * isEquiv A B f @@ -28,26 +14,18 @@ equiv (A B : U) : U = (f : A -> B) * isEquiv A B f propIsEquiv (A B : U) (f : A -> B) : prop (isEquiv A B f) = \ (u0 u1:isEquiv A B f) -> \ (y:B) -> propIsContr (fiber A B f y) (u0 y) (u1 y) @ i -lemPropF (A : U) (P : A -> U) (pP : (x : A) -> prop (P x)) (a0 a1 :A) - (p : Id A a0 a1) (b0 : P a0) (b1 : P a1) : IdP (P (p@i)) b0 b1 = - pP (p@i) (comp (P (p@i/\j)) b0 [(i=0) -> <_>b0]) (comp (P (p@i\/-j)) b1 [(i=1) -> <_>b1])@i - -lemSig (A : U) (B : A -> U) (pB : (x : A) -> prop (B x)) - (u v : (x:A) * B x) (p : Id A u.1 v.1) : - Id ((x:A) * B x) u v = - (p@i,(lemPropF A B pB u.1 v.1 p u.2 v.2)@i) - -propSig (A : U) (B : A -> U) (pA : prop A) - (pB : (x : A) -> prop (B x)) (t u : (x:A) * B x) : - Id ((x:A) * B x) t u = - lemSig A B pB t u (pA t.1 u.1) - equivLemma (A B : U) : (v w : equiv A B) -> Id (A -> B) v.1 w.1 -> Id (equiv A B) v w = lemSig (A -> B) (isEquiv A B) (propIsEquiv A B) --- for univalence +idIsEquiv (A : U) : isEquiv A A (idfun A) = + \(a : A) -> ((a, refl A a) + ,\(z : fiber A A (idfun A) a) -> contrSingl A a z.1 z.2) +equivId (T A : U) (f : T -> A) (p : isEquiv T A f) : Id U T A = + glue A [ (i=0) -> (T,f,p), (i=1) -> (A,idfun A, idIsEquiv A)] + +-- for univalence invEq (A B:U) (w:equiv A B) (y:B) : A = (w.2 y).1.1 retEq (A B:U) (w:equiv A B) (y:B) : Id B (w.1 (invEq A B w y)) y = @@ -56,8 +34,6 @@ retEq (A B:U) (w:equiv A B) (y:B) : Id B (w.1 (invEq A B w y)) y = secEq (A B:U) (w:equiv A B) (x:A) : Id A (invEq A B w (w.1 x)) x = ((w.2 (w.1 x)).2 (x,w.1 x)@i).1 --- transDelta (A:U) : equiv A A = - transEquiv (A B:U) (p:Id U A B) : equiv A B = (f,p) where f (x:A) : B = comp p x [] @@ -104,8 +80,6 @@ eqToEq (A B : U) (p : Id U A B) , (i = 1) -> (B,f) , (j = 1) -> (p@i,g)] -test (A B : U) (w : equiv A B) (x:A) : B = (transEquiv A B (transEquivToId A B w)).1 x - transIdFun (A B : U) (w : equiv A B) : Id (A -> B) w.1 (transEquiv A B (transEquivToId A B w)).1 = \ (a:A) -> @@ -120,6 +94,9 @@ idToId (A B : U) (w : equiv A B) = equivLemma A B (transEquiv A B (transEquivToId A B w)) w (transIdFun A B w@-i) + +-- The grad lemma + lemIso (A B : U) (f : A -> B) (g : B -> A) (s : (y : B) -> Id B (f (g y)) y) (t : (x : A) -> Id A (g (f x)) x) @@ -172,9 +149,11 @@ lemIso (A B : U) (f : A -> B) (g : B -> A) gradLemma (A B : U) (f : A -> B) (g : B -> A) (s : (y : B) -> Id B (f (g y)) y) (t : (x : A) -> Id A (g (f x)) x) : 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) - -transEquivIsEquiv (A B : U) - : isEquiv (Id U A B) (equiv A B) (transEquiv A B) - = gradLemma (Id U A B) (equiv A B) (transEquiv A B) - (transEquivToId A B) (idToId A B) (eqToEq A B) + \(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) + +isoId (A B : U) (f : A -> B) (g : B -> A) + (s : (y : B) -> Id B (f (g y)) y) + (t : (x : A) -> Id A (g (f x)) x) : Id U A B = + glue B [ (i = 0) -> (A,f,gradLemma A B f g s t) + , (i = 1) -> (B,idfun B,idIsEquiv B) ] diff --git a/examples/prelude.ctt b/examples/prelude.ctt index 26779a5..f452fb2 100644 --- a/examples/prelude.ctt +++ b/examples/prelude.ctt @@ -186,6 +186,21 @@ propIsContr (A : U) : prop (isContr A) = lemProp (isContr A) rem pB (x : A) : prop (T x) = propPi A (\ (y : A) -> Id A x y) (propSet A pA x) + +-- Alternative proof: +-- propIsContr (A:U) (z0 z1:isContr A) : Id (isContr A) z0 z1 = +-- (p0 a1@j, +-- \ (x:A) -> +-- comp (<_>A) (lem1 x@i@j) [ (i=0) -> p0 a1@j, (i=1) -> p0 x@(j\/k), +-- (j=0) -> p0 x@(i/\k), (j=1) -> p1 x@i ]) +-- where +-- a0 : A = z0.1 +-- p0 : (x:A) -> Id A a0 x = z0.2 +-- a1 : A = z1.1 +-- p1 : (x:A) -> Id A a1 x = z1.2 +-- lem1 (x:A) : IdP (Id A a0 (p1 x@i)) (p0 a1) (p0 x) = p0 (p1 x@i) @ j + + -- Basic data types data N0 = @@ -244,84 +259,3 @@ and (A B : U) : U = (_ : A) * B propAnd (A B : U) (pA : prop A) (pB : prop B) : prop (and A B) = propSig A (\(_ : A) -> B) pA (\(_ : A) -> pB) -fiber (A B : U) (f : A -> B) (y : B) : U = - (x : A) * Id B y (f x) - -isEquiv (A B : U) (f : A -> B) : U = - (y : B) -> isContr (fiber A B f y) - -idIsEquiv (A : U) : isEquiv A A (idfun A) = - \ (a : A) -> - ((a, refl A a) - , \ (z : fiber A A (idfun A) a) -> contrSingl A a z.1 z.2) - - -equivId (T A : U) (f : T -> A) (p : isEquiv T A f) : Id U T A = - glue A [ (i=0) -> (T,f,p), (i=1) -> (A,idfun A, idIsEquiv A)] - - - ---- isoId - -lemIso (A B : U) (f : A -> B) (g : B -> A) - (s : (y : B) -> Id B (f (g y)) y) - (t : (x : A) -> Id A (g (f x)) x) - (y : B) (x0 x1 : A) (p0 : Id B y (f x0)) (p1 : Id B y (f x1)) : - Id (fiber A B f y) (x0,p0) (x1,p1) = (p @ i,sq1 @ i) - where - rem0 : Id A (g y) x0 = - comp (<_> A) (g (p0 @ i)) [ (i = 1) -> t x0, (i = 0) -> <_> g y ] - - rem1 : Id A (g y) x1 = - comp (<_> A) (g (p1 @ i)) [ (i = 1) -> t x1, (i = 0) -> <_> g y ] - - p : Id 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 ] - -gradLemma (A B : U) (f : A -> B) (g : B -> A) - (s : (y : B) -> Id B (f (g y)) y) - (t : (x : A) -> Id A (g (f x)) x) : 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) - - - -isoId (A B : U) (f : A -> B) (g : B -> A) - (s : (y : B) -> Id B (f (g y)) y) - (t : (x : A) -> Id A (g (f x)) x) : Id U A B = - glue B [ (i = 0) -> (A,f,gradLemma A B f g s t) - , (i = 1) -> (B,idfun B,idIsEquiv B) ] - diff --git a/examples/testContr.ctt b/examples/testContr.ctt deleted file mode 100644 index 5bd7bc4..0000000 --- a/examples/testContr.ctt +++ /dev/null @@ -1,175 +0,0 @@ -module testContr where - -import prelude - -retIsContr (A B :U) (f:A->B) (g:B->A) (h : (x:A) -> Id A (g (f x)) x) (v:isContr B) - : isContr A = (g b,p) - where - b : B = v.1 - q : (y:B) -> Id B b y = v.2 - p (x:A) : Id A (g b) x = comp (A) (g (q (f x)@i)) [(i=0) -> g b,(i=1) -> h x] - -sigIsContr (A:U) (B:A->U) (u:isContr A) (q:(x:A) -> isContr (B x)) - : isContr ((x:A)*B x) = ((a,g a),r) - where - a : A = u.1 - p : (x:A) -> Id A a x = u.2 - g (x:A) : B x = (q x).1 - h (x:A) : (y:B x) -> Id (B x) (g x) y = (q x).2 - C : U = (x:A) * B x - r (z:C) : Id C (a,g a) z = - (p z.1@i,h (p z.1@i) (comp (B (p z.1@i\/-j)) z.2 [(i=1)->z.2])@i) - -isPathContr (A:U) (cA:isContr A) (x y:A) : isContr (Id A x y) = (p0,q) - where - a : A = cA.1 - f : (x:A) -> Id A a x = cA.2 - p0 : Id A x y = comp (A) a [(i=0) -> f x,(i=1) -> f y] - q (p:Id A x y) : Id (Id A x y) p0 p = - comp (A) a [(i=0) -> f x,(i=1) -> f y, - (j=0) -> comp (A) a [(k=0) -> a,(i=0) -> f x@k/\l,(i=1) -> f y@k/\l], - (j=1) -> f (p@i)] - -fiber (A B : U) (f : A -> B) (y : B) : U = - (x : A) * Id B y (f x) - -isEquiv (A B : U) (f : A -> B) : U = (y:B) -> isContr (fiber A B f y) - -equiv (A B : U) : U = (f : A -> B) * isEquiv A B f - -isEquivContr (A B:U) (cA:isContr A) (cB:isContr B) (f:A->B) : isEquiv A B f = - \ (y:B) -> sigIsContr A (\ (x:A) -> Id B y (f x)) cA (\ (x:A) -> isPathContr B cB y (f x)) - -sig (A:U) (B:A->U) : U = (x:A) * B x - -totalFun (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (w:sig A B) : sig A C = - (w.1,f (w.1) (w.2)) - -funFib1 (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (x0:A) (z0:C x0) (u:fiber (B x0) (C x0) (f x0) z0) : - fiber (sig A B) (sig A C) (totalFun A B C f) (x0,z0) = ((x0,u.1),(x0,u.2@i)) - -funFib2 (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (x0:A) (z0:C x0) - (w : fiber (sig A B) (sig A C) (totalFun A B C f) (x0,z0)) : fiber (B x0) (C x0) (f x0) z0 = (b0,s) - where - x : A = w.1.1 - b : B x = w.1.2 - p : Id A x0 x = (w.2@i).1 - q : IdP (C (p@i)) z0 (f x b) = (w.2@i).2 - b0 : B x0 = comp (B (p@-i)) b [] - r : IdP (B (p@-i)) b b0 = comp (B (p@-j\/-i)) b [(i=0) -> b] - s : Id (C x0) z0 (f x0 b0) = comp (C (p@(i/\-j))) (q@i) [(i=0) -> z0,(i=1) -> f (p@-k) (r@k)] - -compFunFib (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (x0:A) (z0:C x0) (u:fiber (B x0) (C x0) (f x0) z0) : - fiber (B x0) (C x0) (f x0) z0 = funFib2 A B C f x0 z0 (funFib1 A B C f x0 z0 u) - -retFunFib (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (x0:A) (z0:C x0) (u:fiber (B x0) (C x0) (f x0) z0) : - Id (fiber (B x0) (C x0) (f x0) z0) (funFib2 A B C f x0 z0 (funFib1 A B C f x0 z0 u)) u = - (comp ( B x0) u.1 [(l=1) -> u.1], - comp ( C x0) (u.2 @ i) [ (l=1) -> u.2 @ i, - (i = 0) -> z0, - (i = 1) -> f x0 (comp ( B x0) u.1 [ (j = 0) -> u.1, (l=1) -> u.1 ]) ]) - -equivFunFib (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (cB : isContr (sig A B)) (cC : isContr (sig A C)) (x:A) - : isEquiv (B x) (C x) (f x) = - \ (z:C x) -> retIsContr (fiber (B x) (C x) (f x) z) (fiber (sig A B) (sig A C) (totalFun A B C f) (x,z)) - (funFib1 A B C f x z) - (funFib2 A B C f x z) - (retFunFib A B C f x z) - (isEquivContr (sig A B) (sig A C) cB cC (totalFun A B C f) (x,z)) - -sig (A : U) (P : A -> U) : U = (x : A) * P x - --- test normal form - -equivFunFib (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (cB : isContr (sig A B)) (cC : isContr (sig A C)) (x:A) - : isEquiv (B x) (C x) (f x) = - \ (z:C x) -> ((comp ( B (comp ( A) cC.1.1 [ (i = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ j).1, (i = 1) -> (cC.2 ((x,z)) @ j).1 ])) cB.1.2 [], comp ( C (comp ( A) cC.1.1 [ (i = 0) -> (cC.2 ((x,z)) @ k).1, (i = 1)(j = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ k).1, (j = 1) -> (cC.2 ((x,z)) @ k).1 ])) (comp ( C (comp ( A) cC.1.1 [ (i = 0) -> (cC.2 ((x,z)) @ (j /\ k)).1, (i = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ k)).1, (j = 0) -> cC.1.1 ])) cC.1.2 [ (i = 0) -> (cC.2 ((x,z)) @ j).2, (i = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ j).2 ]) [ (i = 0) -> z, (i = 1) -> f (comp ( A) cC.1.1 [ (j = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ k).1, (j = 1) -> (cC.2 ((x,z)) @ k).1 ]) (comp ( B (comp ( A) cC.1.1 [ (j = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1, (j = 1)(k = 1) -> (cC.2 ((x,z)) @ i).1, (k = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1 ])) cB.1.2 [ (j = 0) -> cB.1.2 ]) ]),\(x0 : sig (B x) (\(x0 : B x) -> IdP ( C x) z (f x x0))) -> (comp ( B x) (comp ( B (comp ( A) cC.1.1 [ (i = 0) -> comp ( A) cC.1.1 [ (j = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (k /\ l)).1, (j = 1) -> (cC.2 ((x,z)) @ (k /\ l)).1, (k = 0) -> cC.1.1 ], (i = 1) -> (cC.2 ((x,x0.2 @ -j)) @ k).1, (j = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ k).1, (j = 1) -> (cC.2 ((x,z)) @ k).1 ])) (cB.2 ((x,x0.1)) @ i).2 []) [ (i = 0) -> comp ( B (comp ( A) cC.1.1 [ (i = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ k).1, (i = 1) -> (cC.2 ((x,z)) @ k).1 ])) cB.1.2 [], (i = 1) -> comp ( B x) x0.1 [ (j = 1) -> x0.1 ] ], comp ( C x) (comp ( C (comp ( A) cC.1.1 [ (i = 0) -> comp ( A) cC.1.1 [ (j = 0) -> cC.1.1, (k = 0) -> (cC.2 ((x,z)) @ (j /\ m)).1, (k = 1)(l = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ m)).1, (l = 1) -> (cC.2 ((x,z)) @ (j /\ m)).1 ], (i = 1) -> (cC.2 ((x,x0.2 @ (-l /\ k))) @ j).1, (k = 0) -> (cC.2 ((x,z)) @ j).1, (k = 1)(l = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ j).1, (l = 1) -> (cC.2 ((x,z)) @ j).1 ])) (comp ( C (comp ( A) cC.1.1 [ (i = 0) -> comp ( A) cC.1.1 [ (j = 0) -> cC.1.1, (k = 0) -> (cC.2 ((x,z)) @ (l /\ j /\ m)).1, (k = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (l /\ j /\ m)).1, (l = 0) -> cC.1.1 ], (i = 1) -> (cC.2 ((x,x0.2 @ k)) @ (l /\ j)).1, (k = 0) -> (cC.2 ((x,z)) @ (l /\ j)).1, (k = 1) -> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ (l /\ j)).1, (l = 0) -> cC.1.1 ])) cC.1.2 [ (i = 0) -> comp ( C (comp ( A) cC.1.1 [ (j = 0) -> cC.1.1, (k = 0) -> (cC.2 ((x,z)) @ (l /\ j /\ m)).1, (k = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (l /\ j /\ m)).1, (l = 0) -> cC.1.1 ])) cC.1.2 [ (k = 0) -> (cC.2 ((x,z)) @ (l /\ j)).2, (k = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (l /\ j)).2, (l = 0) -> cC.1.2 ], (i = 1) -> (cC.2 ((x,x0.2 @ k)) @ l).2, (k = 0) -> (cC.2 ((x,z)) @ l).2, (k = 1) -> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ l).2 ]) [ (k = 0) -> z, (k = 1) -> f (comp ( A) cC.1.1 [ (i = 0) -> comp ( A) cC.1.1 [ (k = 0) -> cC.1.1, (l = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (k /\ j)).1, (l = 1) -> (cC.2 ((x,z)) @ (k /\ j)).1 ], (i = 1) -> (cC.2 ((x,x0.2 @ -l)) @ k).1, (l = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ k).1, (l = 1) -> (cC.2 ((x,z)) @ k).1 ]) (comp ( B (comp ( A) cC.1.1 [ (i = 0) -> comp ( A) cC.1.1 [ (j = 0) -> cC.1.1, (k = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ m)).1, (k = 1)(l = 1) -> (cC.2 ((x,z)) @ (j /\ m)).1, (l = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ m)).1 ], (i = 1) -> (cC.2 ((x,x0.2 @ (-l \/ -k))) @ j).1, (k = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ j).1, (k = 1)(l = 1) -> (cC.2 ((x,z)) @ j).1, (l = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ j).1 ])) (cB.2 ((x,x0.1)) @ i).2 [ (l = 0) -> (cB.2 ((x,x0.1)) @ i).2 ]) ]) [ (i = 0) -> comp ( C (comp ( A) cC.1.1 [ (j = 0)(k = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1, (j = 1) -> (cC.2 ((x,z)) @ i).1, (k = 0) -> (cC.2 ((x,z)) @ i).1 ])) (comp ( C (comp ( A) cC.1.1 [ (j = 0) -> cC.1.1, (k = 0) -> (cC.2 ((x,z)) @ (j /\ i)).1, (k = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ i)).1 ])) cC.1.2 [ (k = 0) -> (cC.2 ((x,z)) @ j).2, (k = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ j).2 ]) [ (k = 0) -> z, (k = 1) -> f (comp ( A) cC.1.1 [ (j = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ l).1, (j = 1) -> (cC.2 ((x,z)) @ l).1 ]) (comp ( B (comp ( A) cC.1.1 [ (j = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1, (j = 1)(l = 1) -> (cC.2 ((x,z)) @ i).1, (l = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1 ])) cB.1.2 [ (j = 0) -> cB.1.2 ]) ], (i = 1) -> comp ( C x) (x0.2 @ k) [ (k = 0) -> z, (k = 1) -> f x (comp ( B x) x0.1 [ (j = 0) -> x0.1, (l = 1) -> x0.1 ]), (l = 1) -> x0.2 @ k ], (k = 0) -> z, (k = 1) -> f x (comp ( B x) (comp ( B (comp ( A) cC.1.1 [ (i = 0) -> comp ( A) cC.1.1 [ (k = 0) -> cC.1.1, (l = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (k /\ j)).1, (l = 1) -> (cC.2 ((x,z)) @ (k /\ j)).1 ], (i = 1) -> (cC.2 ((x,x0.2 @ -l)) @ k).1, (l = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ k).1, (l = 1) -> (cC.2 ((x,z)) @ k).1 ])) (cB.2 ((x,x0.1)) @ i).2 []) [ (i = 0) -> comp ( B (comp ( A) cC.1.1 [ (i = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ k).1, (i = 1) -> (cC.2 ((x,z)) @ k).1 ])) cB.1.2 [], (i = 1) -> comp ( B x) x0.1 [ (k = 1)(l = 1) -> x0.1 ], (l = 0) -> comp ( B (comp ( A) cC.1.1 [ (i = 0) -> comp ( A) cC.1.1 [ (k = 0) -> cC.1.1, (l = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (k /\ j)).1, (l = 1) -> (cC.2 ((x,z)) @ (k /\ j)).1 ], (i = 1) -> (cC.2 ((x,x0.2 @ -l)) @ k).1, (l = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ k).1, (l = 1) -> (cC.2 ((x,z)) @ k).1 ])) (cB.2 ((x,x0.1)) @ i).2 [] ]) ])) - - - -lemSinglContr (A:U) (a:A) : isContr ((x:A) * Id A a x) = - ((a,refl A a),\ (z:(x:A) * Id A a x) -> contrSingl A a z.1 z.2) - -idEquiv (A:U) : equiv A A = (\ (x:A) -> x, lemSinglContr A) - -lem1 (B:U) : isContr ((X:U) * equiv X B) = - ((B,idEquiv B) - ,\(w : (X : U) * equiv X B) - -> let glueB : U = glue B [(i=0) -> (B,idEquiv B), (i=1) -> w] - unglueElemB : glueB -> B - = \(g : glueB) - -> unglueElem g [(i=0) -> (B,idEquiv B) - ,(i=1) -> w] - in (glueB - ,unglueElemB - ,\(b : B) - -> let center : fiber glueB B unglueElemB b - = (glueElem (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]) - contr (v : fiber glueB B unglueElemB b) - : Id (fiber glueB B unglueElemB b) center v - = (glueElem (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]) - in (center,contr))) - -contrSingl (A : U) (a b : A) (p : Id A a b) : - Id ((x:A) * Id A x b) (b,refl A b) (a,p) = (p @ -i, p @ -i\/j) - -lemSinglContr1 (A:U) (a:A) : isContr ((x:A) * Id A x a) = - ((a,refl A a),\ (z:(x:A) * Id A x a) -> contrSingl A z.1 a z.2) - -thmUniv (t : (A X:U) -> Id U X A -> equiv X A) (A:U) : (X:U) -> isEquiv (Id U X A) (equiv X A) (t A X) = - equivFunFib U (\ (X:U) -> Id U X A) (\ (X:U) -> equiv X A) (t A) (lemSinglContr1 U A) (lem1 A) - -lem2 (A X:U) (p:Id U X A) : equiv X A = substTrans U (\ (Y:U) -> equiv Y A) A X (p@-i) (idEquiv A) - -univalence (A X:U) : isEquiv (Id U X A) (equiv X A) (lem2 A X) = thmUniv lem2 A X - -corrUniv (A X:U) : Id U (Id U X A) (equiv X A) = - equivId (Id U X A) (equiv X A) (lem2 A X) (univalence A X) - -corrUniv' (A B : U) : equiv (Id U A B) (equiv A B) = (lem2 B A,univalence B A) - -testUniv1 (A:U) : Id U A A = trans (equiv A A) (Id U A A) (corrUniv A A@-i) (idEquiv A) - --- obtained by normal form - -testUniv1 (A:U) : Id U A A = - comp (<_>U) - (comp (<_>U) A - [ (i = 0) -> comp (<_>U) A [ (l = 0) -> glue A [ (i = 0) -> (A,(\(x : A) -> x,\(a : A) -> ((a, a),\(z : ((x : A) * IdP ( A) a x)) -> (z.2 @ l, z.2 @ (l /\ i))))), (i = 1) -> (A,(comp ( A -> A) (\(x : A) -> x) [],comp ( (y : A) -> - ((x : ((x : A) * IdP ( A) y (comp ( A) (comp ( A) x []) [ (l = 0) -> comp ( A) x [ (j = 1) -> x ] ]))) * (y0 : ((x0 : A) * IdP ( A) y (comp ( A) (comp ( A) x0 []) [ (l = 0) -> comp ( A) x0 [ (j = 1) -> x0 ] ]))) -> IdP ( ((x0 : A) * IdP ( A) y (comp ( A) (comp ( A) x0 []) [ (l = 0) -> comp ( A) x0 [ (j = 1) -> x0 ] ]))) x y0)) (\(a : A) -> ((a, a),\(z : ((x : A) * IdP ( A) a x)) -> (z.2 @ l, z.2 @ (l /\ i)))) [])) ], (l = 1) -> glue A [ (i = 0) -> (A,(\(x : A) -> x,\(a : A) -> ((a, a),\(z : ((x : A) * IdP ( A) a x)) -> (z.2 @ l, z.2 @ (l /\ i))))), (i = 1) -> (A,(comp ( A -> A) (\(x : A) -> x) [],comp ( (y : A) -> - ((x : ((x : A) * IdP ( A) y (comp ( A) (comp ( A) x []) [ (l = 0) -> comp ( A) x [ (j = 1) -> x ] ]))) * (y0 : ((x0 : A) * IdP ( A) y (comp ( A) (comp ( A) x0 []) [ (l = 0) -> comp ( A) x0 [ (j = 1) -> x0 ] ]))) -> IdP ( ((x0 : A) * IdP ( A) y (comp ( A) (comp ( A) x0 []) [ (l = 0) -> comp ( A) x0 [ (j = 1) -> x0 ] ]))) x y0)) (\(a : A) -> ((a, a),\(z : ((x : A) * IdP ( A) a x)) -> (z.2 @ l, z.2 @ (l /\ i)))) [])) ] ], (i = 1) -> A ]) [ (i = 0) -> A, (i = 1) -> A ] - -data bool = true | false - -testUniv2 : bool = trans bool bool (testUniv1 bool) true - -testUniv2 : bool = - comp ( comp (<_>U) (comp (<_>U) bool [ (i = 0) -> comp (<_>U) bool [ (j = 0) -> glue bool [ (i = 0) -> (bool,(\(x : bool) -> x,\(a : bool) -> ((a, a),\(z : ((x : bool) * IdP ( bool) a x)) -> (z.2 @ i, z.2 @ (i /\ j))))), (i = 1) -> (bool,(comp ( bool -> bool) (\(x : bool) -> x) [],comp ( (y : bool) -> - ((x : ((x : bool) * IdP ( bool) y (comp ( bool) (comp ( bool) x []) [ (i = 0) -> comp ( bool) x [ (j = 1) -> x ] ]))) * (y0 : ((x0 : bool) * IdP ( bool) y (comp ( bool) (comp ( bool) x0 []) [ (i = 0) -> comp ( bool) x0 [ (j = 1) -> x0 ] ]))) -> IdP ( ((x0 : bool) * IdP ( bool) y (comp ( bool) (comp ( bool) x0 []) [ (i = 0) -> comp ( bool) x0 [ (j = 1) -> x0 ] ]))) x y0)) (\(a : bool) -> ((a, a),\(z : ((x : bool) * IdP ( bool) a x)) -> (z.2 @ i, z.2 @ (i /\ j)))) [])) ], (j = 1) -> glue bool [ (i = 0) -> (bool,(\(x : bool) -> x,\(a : bool) -> ((a, a),\(z : ((x : bool) * IdP ( bool) a x)) -> (z.2 @ i, z.2 @ (i /\ j))))), (i = 1) -> (bool,(comp ( bool -> bool) (\(x : bool) -> x) [],comp ( (y : bool) -> - ((x : ((x : bool) * IdP ( bool) y (comp ( bool) (comp ( bool) x []) [ (i = 0) -> comp ( bool) x [ (j = 1) -> x ] ]))) * (y0 : ((x0 : bool) * IdP ( bool) y (comp ( bool) (comp ( bool) x0 []) [ (i = 0) -> comp ( bool) x0 [ (j = 1) -> x0 ] ]))) -> IdP ( ((x0 : bool) * IdP ( bool) y (comp ( bool) (comp ( bool) x0 []) [ (i = 0) -> comp ( bool) x0 [ (j = 1) -> x0 ] ]))) x y0)) (\(a : bool) -> ((a, a),\(z : ((x : bool) * IdP ( bool) a x)) -> (z.2 @ i, z.2 @ (i /\ j)))) [])) ] ], (i = 1) -> bool ]) [ (i = 0) -> bool, (i = 1) -> bool ]) true [] - - - - - - - --- thmUniv (lem1 : (A:U) -> isContr ((X:U) * equiv A X)) (t : (A X:U) -> Id U A X -> equiv A X) (A:U) --- : (X:U) -> isEquiv (Id U A X) (equiv A X) (t A X) = --- equivFunFib U (\ (X:U) -> Id U A X) (equiv A) (t A) (lemSinglContr U A) (lem1 A) diff --git a/examples/univalence.ctt b/examples/univalence.ctt new file mode 100644 index 0000000..513591a --- /dev/null +++ b/examples/univalence.ctt @@ -0,0 +1,222 @@ +-- This file contains two proofs of univalence. One using unglue +-- (section ? of the cubicaltt paper) and a direct one... +module univalence where + +import equiv +import bool + +------------------------------------------------------------------------------ +-- Proof of univalence using unglue: + +retIsContr (A B :U) (f:A->B) (g:B->A) (h : (x:A) -> Id A (g (f x)) x) (v:isContr B) + : isContr A = (g b,p) + where + b : B = v.1 + q : (y:B) -> Id B b y = v.2 + p (x:A) : Id A (g b) x = comp (A) (g (q (f x)@i)) [(i=0) -> g b,(i=1) -> h x] + +sigIsContr (A:U) (B:A->U) (u:isContr A) (q:(x:A) -> isContr (B x)) + : isContr ((x:A)*B x) = ((a,g a),r) + where + a : A = u.1 + p : (x:A) -> Id A a x = u.2 + g (x:A) : B x = (q x).1 + h (x:A) : (y:B x) -> Id (B x) (g x) y = (q x).2 + C : U = (x:A) * B x + r (z:C) : Id C (a,g a) z = + (p z.1@i,h (p z.1@i) (comp (B (p z.1@i\/-j)) z.2 [(i=1)->z.2])@i) + +isPathContr (A:U) (cA:isContr A) (x y:A) : isContr (Id A x y) = (p0,q) + where + a : A = cA.1 + f : (x:A) -> Id A a x = cA.2 + p0 : Id A x y = comp (A) a [(i=0) -> f x,(i=1) -> f y] + q (p:Id A x y) : Id (Id A x y) p0 p = + comp (A) a [(i=0) -> f x,(i=1) -> f y, + (j=0) -> comp (A) a [(k=0) -> a,(i=0) -> f x@k/\l,(i=1) -> f y@k/\l], + (j=1) -> f (p@i)] + +isEquivContr (A B:U) (cA:isContr A) (cB:isContr B) (f:A->B) : isEquiv A B f = + \ (y:B) -> sigIsContr A (\ (x:A) -> Id B y (f x)) cA (\ (x:A) -> isPathContr B cB y (f x)) + +sig (A:U) (B:A->U) : U = (x:A) * B x + +totalFun (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (w:sig A B) : sig A C = + (w.1,f (w.1) (w.2)) + +funFib1 (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (x0:A) (z0:C x0) (u:fiber (B x0) (C x0) (f x0) z0) : + fiber (sig A B) (sig A C) (totalFun A B C f) (x0,z0) = ((x0,u.1),(x0,u.2@i)) + +funFib2 (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (x0:A) (z0:C x0) + (w : fiber (sig A B) (sig A C) (totalFun A B C f) (x0,z0)) : fiber (B x0) (C x0) (f x0) z0 = (b0,s) + where + x : A = w.1.1 + b : B x = w.1.2 + p : Id A x0 x = (w.2@i).1 + q : IdP (C (p@i)) z0 (f x b) = (w.2@i).2 + b0 : B x0 = comp (B (p@-i)) b [] + r : IdP (B (p@-i)) b b0 = comp (B (p@-j\/-i)) b [(i=0) -> b] + s : Id (C x0) z0 (f x0 b0) = comp (C (p@(i/\-j))) (q@i) [(i=0) -> z0,(i=1) -> f (p@-k) (r@k)] + +compFunFib (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (x0:A) (z0:C x0) (u:fiber (B x0) (C x0) (f x0) z0) : + fiber (B x0) (C x0) (f x0) z0 = funFib2 A B C f x0 z0 (funFib1 A B C f x0 z0 u) + +retFunFib (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (x0:A) (z0:C x0) (u:fiber (B x0) (C x0) (f x0) z0) : + Id (fiber (B x0) (C x0) (f x0) z0) (funFib2 A B C f x0 z0 (funFib1 A B C f x0 z0 u)) u = + (comp ( B x0) u.1 [(l=1) -> u.1], + comp ( C x0) (u.2 @ i) [ (l=1) -> u.2 @ i, + (i = 0) -> z0, + (i = 1) -> f x0 (comp ( B x0) u.1 [ (j = 0) -> u.1, (l=1) -> u.1 ]) ]) + +equivFunFib (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (cB : isContr (sig A B)) (cC : isContr (sig A C)) (x:A) + : isEquiv (B x) (C x) (f x) = + \ (z:C x) -> retIsContr (fiber (B x) (C x) (f x) z) (fiber (sig A B) (sig A C) (totalFun A B C f) (x,z)) + (funFib1 A B C f x z) + (funFib2 A B C f x z) + (retFunFib A B C f x z) + (isEquivContr (sig A B) (sig A C) cB cC (totalFun A B C f) (x,z)) + +-- test normal form + +-- equivFunFib (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (cB : isContr (sig A B)) (cC : isContr (sig A C)) (x:A) +-- : isEquiv (B x) (C x) (f x) = +-- \ (z:C x) -> ((comp ( B (comp ( A) cC.1.1 [ (i = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ j).1, (i = 1) -> (cC.2 ((x,z)) @ j).1 ])) cB.1.2 [], comp ( C (comp ( A) cC.1.1 [ (i = 0) -> (cC.2 ((x,z)) @ k).1, (i = 1)(j = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ k).1, (j = 1) -> (cC.2 ((x,z)) @ k).1 ])) (comp ( C (comp ( A) cC.1.1 [ (i = 0) -> (cC.2 ((x,z)) @ (j /\ k)).1, (i = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ k)).1, (j = 0) -> cC.1.1 ])) cC.1.2 [ (i = 0) -> (cC.2 ((x,z)) @ j).2, (i = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ j).2 ]) [ (i = 0) -> z, (i = 1) -> f (comp ( A) cC.1.1 [ (j = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ k).1, (j = 1) -> (cC.2 ((x,z)) @ k).1 ]) (comp ( B (comp ( A) cC.1.1 [ (j = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1, (j = 1)(k = 1) -> (cC.2 ((x,z)) @ i).1, (k = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1 ])) cB.1.2 [ (j = 0) -> cB.1.2 ]) ]),\(x0 : sig (B x) (\(x0 : B x) -> IdP ( C x) z (f x x0))) -> (comp ( B x) (comp ( B (comp ( A) cC.1.1 [ (i = 0) -> comp ( A) cC.1.1 [ (j = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (k /\ l)).1, (j = 1) -> (cC.2 ((x,z)) @ (k /\ l)).1, (k = 0) -> cC.1.1 ], (i = 1) -> (cC.2 ((x,x0.2 @ -j)) @ k).1, (j = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ k).1, (j = 1) -> (cC.2 ((x,z)) @ k).1 ])) (cB.2 ((x,x0.1)) @ i).2 []) [ (i = 0) -> comp ( B (comp ( A) cC.1.1 [ (i = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ k).1, (i = 1) -> (cC.2 ((x,z)) @ k).1 ])) cB.1.2 [], (i = 1) -> comp ( B x) x0.1 [ (j = 1) -> x0.1 ] ], comp ( C x) (comp ( C (comp ( A) cC.1.1 [ (i = 0) -> comp ( A) cC.1.1 [ (j = 0) -> cC.1.1, (k = 0) -> (cC.2 ((x,z)) @ (j /\ m)).1, (k = 1)(l = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ m)).1, (l = 1) -> (cC.2 ((x,z)) @ (j /\ m)).1 ], (i = 1) -> (cC.2 ((x,x0.2 @ (-l /\ k))) @ j).1, (k = 0) -> (cC.2 ((x,z)) @ j).1, (k = 1)(l = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ j).1, (l = 1) -> (cC.2 ((x,z)) @ j).1 ])) (comp ( C (comp ( A) cC.1.1 [ (i = 0) -> comp ( A) cC.1.1 [ (j = 0) -> cC.1.1, (k = 0) -> (cC.2 ((x,z)) @ (l /\ j /\ m)).1, (k = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (l /\ j /\ m)).1, (l = 0) -> cC.1.1 ], (i = 1) -> (cC.2 ((x,x0.2 @ k)) @ (l /\ j)).1, (k = 0) -> (cC.2 ((x,z)) @ (l /\ j)).1, (k = 1) -> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ (l /\ j)).1, (l = 0) -> cC.1.1 ])) cC.1.2 [ (i = 0) -> comp ( C (comp ( A) cC.1.1 [ (j = 0) -> cC.1.1, (k = 0) -> (cC.2 ((x,z)) @ (l /\ j /\ m)).1, (k = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (l /\ j /\ m)).1, (l = 0) -> cC.1.1 ])) cC.1.2 [ (k = 0) -> (cC.2 ((x,z)) @ (l /\ j)).2, (k = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (l /\ j)).2, (l = 0) -> cC.1.2 ], (i = 1) -> (cC.2 ((x,x0.2 @ k)) @ l).2, (k = 0) -> (cC.2 ((x,z)) @ l).2, (k = 1) -> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ l).2 ]) [ (k = 0) -> z, (k = 1) -> f (comp ( A) cC.1.1 [ (i = 0) -> comp ( A) cC.1.1 [ (k = 0) -> cC.1.1, (l = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (k /\ j)).1, (l = 1) -> (cC.2 ((x,z)) @ (k /\ j)).1 ], (i = 1) -> (cC.2 ((x,x0.2 @ -l)) @ k).1, (l = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ k).1, (l = 1) -> (cC.2 ((x,z)) @ k).1 ]) (comp ( B (comp ( A) cC.1.1 [ (i = 0) -> comp ( A) cC.1.1 [ (j = 0) -> cC.1.1, (k = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ m)).1, (k = 1)(l = 1) -> (cC.2 ((x,z)) @ (j /\ m)).1, (l = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ m)).1 ], (i = 1) -> (cC.2 ((x,x0.2 @ (-l \/ -k))) @ j).1, (k = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ j).1, (k = 1)(l = 1) -> (cC.2 ((x,z)) @ j).1, (l = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ j).1 ])) (cB.2 ((x,x0.1)) @ i).2 [ (l = 0) -> (cB.2 ((x,x0.1)) @ i).2 ]) ]) [ (i = 0) -> comp ( C (comp ( A) cC.1.1 [ (j = 0)(k = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1, (j = 1) -> (cC.2 ((x,z)) @ i).1, (k = 0) -> (cC.2 ((x,z)) @ i).1 ])) (comp ( C (comp ( A) cC.1.1 [ (j = 0) -> cC.1.1, (k = 0) -> (cC.2 ((x,z)) @ (j /\ i)).1, (k = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ i)).1 ])) cC.1.2 [ (k = 0) -> (cC.2 ((x,z)) @ j).2, (k = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ j).2 ]) [ (k = 0) -> z, (k = 1) -> f (comp ( A) cC.1.1 [ (j = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ l).1, (j = 1) -> (cC.2 ((x,z)) @ l).1 ]) (comp ( B (comp ( A) cC.1.1 [ (j = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1, (j = 1)(l = 1) -> (cC.2 ((x,z)) @ i).1, (l = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1 ])) cB.1.2 [ (j = 0) -> cB.1.2 ]) ], (i = 1) -> comp ( C x) (x0.2 @ k) [ (k = 0) -> z, (k = 1) -> f x (comp ( B x) x0.1 [ (j = 0) -> x0.1, (l = 1) -> x0.1 ]), (l = 1) -> x0.2 @ k ], (k = 0) -> z, (k = 1) -> f x (comp ( B x) (comp ( B (comp ( A) cC.1.1 [ (i = 0) -> comp ( A) cC.1.1 [ (k = 0) -> cC.1.1, (l = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (k /\ j)).1, (l = 1) -> (cC.2 ((x,z)) @ (k /\ j)).1 ], (i = 1) -> (cC.2 ((x,x0.2 @ -l)) @ k).1, (l = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ k).1, (l = 1) -> (cC.2 ((x,z)) @ k).1 ])) (cB.2 ((x,x0.1)) @ i).2 []) [ (i = 0) -> comp ( B (comp ( A) cC.1.1 [ (i = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ k).1, (i = 1) -> (cC.2 ((x,z)) @ k).1 ])) cB.1.2 [], (i = 1) -> comp ( B x) x0.1 [ (k = 1)(l = 1) -> x0.1 ], (l = 0) -> comp ( B (comp ( A) cC.1.1 [ (i = 0) -> comp ( A) cC.1.1 [ (k = 0) -> cC.1.1, (l = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (k /\ j)).1, (l = 1) -> (cC.2 ((x,z)) @ (k /\ j)).1 ], (i = 1) -> (cC.2 ((x,x0.2 @ -l)) @ k).1, (l = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ k).1, (l = 1) -> (cC.2 ((x,z)) @ k).1 ])) (cB.2 ((x,x0.1)) @ i).2 [] ]) ])) + +-- lemSinglContr (A:U) (a:A) : isContr ((x:A) * Id A a x) = +-- ((a,refl A a),\ (z:(x:A) * Id A a x) -> contrSingl A a z.1 z.2) + +-- idEquiv (A:U) : equiv A A = (\ (x:A) -> x, lemSinglContr A) + +lem1 (B:U) : isContr ((X:U) * equiv X B) = + ((B,idEquiv B) + ,\(w : (X : U) * equiv X B) + -> let glueB : U = glue B [(i=0) -> (B,idEquiv B), (i=1) -> w] + unglueElemB : glueB -> B + = \(g : glueB) + -> unglueElem g [(i=0) -> (B,idEquiv B) + ,(i=1) -> w] + in (glueB + ,unglueElemB + ,\(b : B) + -> let center : fiber glueB B unglueElemB b + = (glueElem (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]) + contr (v : fiber glueB B unglueElemB b) + : Id (fiber glueB B unglueElemB b) center v + = (glueElem (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]) + in (center,contr))) + +contrSingl' (A : U) (a b : A) (p : Id A a b) : + Id ((x:A) * Id A x b) (b,refl A b) (a,p) = (p @ -i, p @ -i\/j) + +lemSinglContr1 (A:U) (a:A) : isContr ((x:A) * Id A x a) = + ((a,refl A a),\ (z:(x:A) * Id A x a) -> contrSingl' A z.1 a z.2) + +thmUniv (t : (A X:U) -> Id U X A -> equiv X A) (A:U) : (X:U) -> isEquiv (Id U X A) (equiv X A) (t A X) = + equivFunFib U (\ (X:U) -> Id U X A) (\ (X:U) -> equiv X A) (t A) (lemSinglContr1 U A) (lem1 A) + +lem2 (A X:U) (p:Id U X A) : equiv X A = substTrans U (\ (Y:U) -> equiv Y A) A X (p@-i) (idEquiv A) + +univalence (A X:U) : isEquiv (Id U X A) (equiv X A) (lem2 A X) = thmUniv lem2 A X + +corrUniv (A X:U) : Id U (Id U X A) (equiv X A) = + equivId (Id U X A) (equiv X A) (lem2 A X) (univalence A X) + +corrUniv' (A B : U) : equiv (Id U A B) (equiv A B) = (lem2 B A,univalence B A) + +testUniv1 (A:U) : Id U A A = + trans (equiv A A) (Id U A A) ( corrUniv A A @ -i) (idEquiv A) + +-- obtained by normal form +ntestUniv1 (A:U) : Id U A A = + comp (<_>U) + (comp (<_>U) A + [ (i = 0) -> comp (<_>U) A [ (l = 0) -> glue A [ (i = 0) -> (A,(\(x : A) -> x,\(a : A) -> ((a, a),\(z : ((x : A) * IdP ( A) a x)) -> (z.2 @ l, z.2 @ (l /\ i))))), (i = 1) -> (A,(comp ( A -> A) (\(x : A) -> x) [],comp ( (y : A) -> + ((x : ((x : A) * IdP ( A) y (comp ( A) (comp ( A) x []) [ (l = 0) -> comp ( A) x [ (j = 1) -> x ] ]))) * (y0 : ((x0 : A) * IdP ( A) y (comp ( A) (comp ( A) x0 []) [ (l = 0) -> comp ( A) x0 [ (j = 1) -> x0 ] ]))) -> IdP ( ((x0 : A) * IdP ( A) y (comp ( A) (comp ( A) x0 []) [ (l = 0) -> comp ( A) x0 [ (j = 1) -> x0 ] ]))) x y0)) (\(a : A) -> ((a, a),\(z : ((x : A) * IdP ( A) a x)) -> (z.2 @ l, z.2 @ (l /\ i)))) [])) ], (l = 1) -> glue A [ (i = 0) -> (A,(\(x : A) -> x,\(a : A) -> ((a, a),\(z : ((x : A) * IdP ( A) a x)) -> (z.2 @ l, z.2 @ (l /\ i))))), (i = 1) -> (A,(comp ( A -> A) (\(x : A) -> x) [],comp ( (y : A) -> + ((x : ((x : A) * IdP ( A) y (comp ( A) (comp ( A) x []) [ (l = 0) -> comp ( A) x [ (j = 1) -> x ] ]))) * (y0 : ((x0 : A) * IdP ( A) y (comp ( A) (comp ( A) x0 []) [ (l = 0) -> comp ( A) x0 [ (j = 1) -> x0 ] ]))) -> IdP ( ((x0 : A) * IdP ( A) y (comp ( A) (comp ( A) x0 []) [ (l = 0) -> comp ( A) x0 [ (j = 1) -> x0 ] ]))) x y0)) (\(a : A) -> ((a, a),\(z : ((x : A) * IdP ( A) a x)) -> (z.2 @ l, z.2 @ (l /\ i)))) [])) ] ], (i = 1) -> A ]) [ (i = 0) -> A, (i = 1) -> A ] + +testUniv2 : bool = trans bool bool (testUniv1 bool) true + +ntestUniv2 : bool = + comp ( comp (<_>U) (comp (<_>U) bool [ (i = 0) -> comp (<_>U) bool [ (j = 0) -> glue bool [ (i = 0) -> (bool,(\(x : bool) -> x,\(a : bool) -> ((a, a),\(z : ((x : bool) * IdP ( bool) a x)) -> (z.2 @ i, z.2 @ (i /\ j))))), (i = 1) -> (bool,(comp ( bool -> bool) (\(x : bool) -> x) [],comp ( (y : bool) -> + ((x : ((x : bool) * IdP ( bool) y (comp ( bool) (comp ( bool) x []) [ (i = 0) -> comp ( bool) x [ (j = 1) -> x ] ]))) * (y0 : ((x0 : bool) * IdP ( bool) y (comp ( bool) (comp ( bool) x0 []) [ (i = 0) -> comp ( bool) x0 [ (j = 1) -> x0 ] ]))) -> IdP ( ((x0 : bool) * IdP ( bool) y (comp ( bool) (comp ( bool) x0 []) [ (i = 0) -> comp ( bool) x0 [ (j = 1) -> x0 ] ]))) x y0)) (\(a : bool) -> ((a, a),\(z : ((x : bool) * IdP ( bool) a x)) -> (z.2 @ i, z.2 @ (i /\ j)))) [])) ], (j = 1) -> glue bool [ (i = 0) -> (bool,(\(x : bool) -> x,\(a : bool) -> ((a, a),\(z : ((x : bool) * IdP ( bool) a x)) -> (z.2 @ i, z.2 @ (i /\ j))))), (i = 1) -> (bool,(comp ( bool -> bool) (\(x : bool) -> x) [],comp ( (y : bool) -> + ((x : ((x : bool) * IdP ( bool) y (comp ( bool) (comp ( bool) x []) [ (i = 0) -> comp ( bool) x [ (j = 1) -> x ] ]))) * (y0 : ((x0 : bool) * IdP ( bool) y (comp ( bool) (comp ( bool) x0 []) [ (i = 0) -> comp ( bool) x0 [ (j = 1) -> x0 ] ]))) -> IdP ( ((x0 : bool) * IdP ( bool) y (comp ( bool) (comp ( bool) x0 []) [ (i = 0) -> comp ( bool) x0 [ (j = 1) -> x0 ] ]))) x y0)) (\(a : bool) -> ((a, a),\(z : ((x : bool) * IdP ( bool) a x)) -> (z.2 @ i, z.2 @ (i /\ j)))) [])) ] ], (i = 1) -> bool ]) [ (i = 0) -> bool, (i = 1) -> bool ]) true [] + + +------------------------------------------------------------------------------ +-- The direct proof of univalence using transEquiv: + +-- transEquiv is an equiv +transEquivIsEquiv (A B : U) + : isEquiv (Id U A B) (equiv A B) (transEquiv A B) + = gradLemma (Id U A B) (equiv A B) (transEquiv A B) + (transEquivToId A B) (idToId A B) (eqToEq A B) + +-- Univalence proved using transEquiv +univalenceTrans (A B:U) : Id U (Id U A B) (equiv A B) = + isoId (Id U A B) (equiv A B) (transEquiv A B) + (transEquivToId A B) (idToId A B) (eqToEq A B) + +univalenceTrans' (A B : U) : equiv (Id U A B) (equiv A B) = + (transEquiv A B,transEquivIsEquiv A B) + +-- univalenceTrans takes extremely much memory when normalizing + +-- This also takes too long to normalize: +slowtest (A : U) : Id (equiv A A) + (transEquiv A A (transEquivToId A A (idEquiv A))) (idEquiv A) = + idToId A A (idEquiv A) + + + + +------------------------------------------------------------------------------ +-- TODO: Adapt this to new definition of equiv + +-- The canonical map defined using J +-- canIdToEquiv (A : U) : (B : U) -> Id U A B -> equiv A B = +-- J U A (\ (B : U) (_ : Id U A B) -> equiv A B) (idEquiv A) + +-- canDiagTrans (A : U) : Id (A -> A) (canIdToEquiv A A (<_> A)).1 (idfun A) = +-- fill (<_> A -> A) (idfun A) [] @ -i + +-- transDiagTrans (A : U) : Id (A -> A) (idfun A) (trans A A (<_> A)) = +-- \ (a : A) -> fill (<_> A) a [] @ i + +-- canIdToEquivLem (A : U) : (B : U) (p : Id U A B) -> +-- Id (A -> B) (canIdToEquiv A B p).1 (transEquiv A B p).1 +-- = J U A +-- (\ (B : U) (p : Id U A B) -> +-- Id (A -> B) (canIdToEquiv A B p).1 (transEquiv A B p).1) +-- (compId (A -> A) +-- (canIdToEquiv A A (<_> A)).1 (idfun A) (trans A A (<_> A)) +-- (canDiagTrans A) (transDiagTrans A)) + +-- canIdToEquivIsTransEquiv (A B : U) : +-- Id (Id U A B -> equiv A B) (canIdToEquiv A B) (transEquiv A B) = +-- \ (p : Id U A B) -> +-- equivLemma A B (canIdToEquiv A B p) (transEquiv A B p) +-- (canIdToEquivLem A B p) @ i + +-- -- The canonical map is an equivalence +-- univalenceJ (A B : U) : isEquiv (Id U A B) (equiv A B) (canIdToEquiv A B) = +-- substInv (Id U A B -> equiv A B) +-- (isEquiv (Id U A B) (equiv A B)) +-- (canIdToEquiv A B) (transEquiv A B) +-- (canIdToEquivIsTransEquiv A B) +-- (transEquivIsEquiv A B) \ No newline at end of file