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 =
- <j>(p0 a1@j,
- \ (x:A) ->
- <i>comp (<_>A) (lem1 x@i@j) [ (i=0) -> <k>p0 a1@j, (i=1) -> <k>p0 x@(j\/k),
- (j=0) -> <k>p0 x@(i/\k), (j=1) -> <k>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 (<i>Id A a0 (p1 x@i)) (p0 a1) (p0 x) = <i j> 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
propIsEquiv (A B : U) (f : A -> B)
: prop (isEquiv A B f) = \ (u0 u1:isEquiv A B f) -> <i> \ (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 (<i>P (p@i)) b0 b1 =
- <i>pP (p@i) (comp (<j>P (p@i/\j)) b0 [(i=0) -> <_>b0]) (comp (<j>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 =
- <i> (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 =
+ <i> 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 =
secEq (A B:U) (w:equiv A B) (x:A) : Id A (invEq A B w (w.1 x)) x =
<i> ((w.2 (w.1 x)).2 (x,<j>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 []
, (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 =
<i> \ (a:A) ->
= equivLemma A B (transEquiv A B (transEquivToId A B w)) w
(<i>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)
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,<i>s y@-i),\ (z:fiber A B f y) -> lemIso A B f g s t y (g y) z.1 (<i>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,<i>s y@-i),\ (z:fiber A B f y) ->
+ lemIso A B f g s t y (g y) z.1 (<i>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 =
+ <i> glue B [ (i = 0) -> (A,f,gradLemma A B f g s t)
+ , (i = 1) -> (B,idfun B,idIsEquiv B) ]
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 =
+-- <j>(p0 a1@j,
+-- \ (x:A) ->
+-- <i>comp (<_>A) (lem1 x@i@j) [ (i=0) -> <k>p0 a1@j, (i=1) -> <k>p0 x@(j\/k),
+-- (j=0) -> <k>p0 x@(i/\k), (j=1) -> <k>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 (<i>Id A a0 (p1 x@i)) (p0 a1) (p0 x) = <i j> p0 (p1 x@i) @ j
+
+
-- Basic data types
data N0 =
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 =
- <i> 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) = <i> (p @ i,sq1 @ i)
- where
- rem0 : Id A (g y) x0 =
- <i> comp (<_> A) (g (p0 @ i)) [ (i = 1) -> t x0, (i = 0) -> <_> g y ]
-
- rem1 : Id A (g y) x1 =
- <i> comp (<_> A) (g (p1 @ i)) [ (i = 1) -> t x1, (i = 0) -> <_> g y ]
-
- p : Id A x0 x1 =
- <i> comp (<_> A) (g y) [ (i = 0) -> rem0
- , (i = 1) -> rem1 ]
-
- fill0 : Square A (g y) (g (f x0)) (g y) x0
- (<i> g (p0 @ i)) rem0 (<i> g y) (t x0) =
- <i j> comp (<_> A) (g (p0 @ i)) [ (i = 1) -> <k> t x0 @ j /\ k
- , (i = 0) -> <_> g y
- , (j = 0) -> <_> g (p0 @ i) ]
-
- fill1 : Square A (g y) (g (f x1)) (g y) x1
- (<i> g (p1 @ i)) rem1 (<i> g y) (t x1) =
- <i j> comp (<_> A) (g (p1 @ i)) [ (i = 1) -> <k> 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 =
- <i j> comp (<_> A) (g y) [ (i = 0) -> <k> rem0 @ j /\ k
- , (i = 1) -> <k> rem1 @ j /\ k
- , (j = 0) -> <_> g y ]
-
- sq : Square A (g y) (g y) (g (f x0)) (g (f x1))
- (<i> g y) (<i> g (f (p @ i)))
- (<j> g (p0 @ j)) (<j> g (p1 @ j)) =
- <i j> comp (<_> A) (fill2 @ i @ j) [ (i = 0) -> <k> fill0 @ j @ -k
- , (i = 1) -> <k> fill1 @ j @ -k
- , (j = 0) -> <_> g y
- , (j = 1) -> <k> t (p @ i) @ -k ]
-
- sq1 : Square B y y (f x0) (f x1)
- (<_>y) (<i> f (p @ i)) p0 p1 =
- <i j> 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,<i>s y@-i),\ (z:fiber A B f y) -> lemIso A B f g s t y (g y) z.1 (<i>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 =
- <i> glue B [ (i = 0) -> (A,f,gradLemma A B f g s t)
- , (i = 1) -> (B,idfun B,idIsEquiv B) ]
-
+++ /dev/null
-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 = <i>comp (<j>A) (g (q (f x)@i)) [(i=0) -> <j>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 =
- <i>(p z.1@i,h (p z.1@i) (comp (<j>B (p z.1@i\/-j)) z.2 [(i=1)-><j>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 = <i>comp (<j>A) a [(i=0) -> f x,(i=1) -> f y]
- q (p:Id A x y) : Id (Id A x y) p0 p =
- <j i>comp (<k>A) a [(i=0) -> f x,(i=1) -> f y,
- (j=0) -> <k>comp (<l>A) a [(k=0) -> <l>a,(i=0) -> <l>f x@k/\l,(i=1) -> <l>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),<i>(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 = <i>(w.2@i).1
- q : IdP (<i>C (p@i)) z0 (f x b) = <i>(w.2@i).2
- b0 : B x0 = comp (<i>B (p@-i)) b []
- r : IdP (<i>B (p@-i)) b b0 = <i>comp (<j>B (p@-j\/-i)) b [(i=0) -> <k>b]
- s : Id (C x0) z0 (f x0 b0) = <i>comp (<j>C (p@(i/\-j))) (q@i) [(i=0) -> <k>z0,(i=1) -> <k>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 =
- <l> (comp (<i> B x0) u.1 [(l=1) -> <j>u.1],
- <i> comp (<j> C x0) (u.2 @ i) [ (l=1) -> <j> u.2 @ i,
- (i = 0) -> <j> z0,
- (i = 1) -> <j> f x0 (comp (<k> B x0) u.1 [ (j = 0) -> <k> u.1, (l=1) -> <k>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 (<i> B (comp (<j> A) cC.1.1 [ (i = 0) -> <j> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ j).1, (i = 1) -> <j> (cC.2 ((x,z)) @ j).1 ])) cB.1.2 [],<i> comp (<j> C (comp (<k> A) cC.1.1 [ (i = 0) -> <k> (cC.2 ((x,z)) @ k).1, (i = 1)(j = 0) -> <k> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ k).1, (j = 1) -> <k> (cC.2 ((x,z)) @ k).1 ])) (comp (<j> C (comp (<k> A) cC.1.1 [ (i = 0) -> <k> (cC.2 ((x,z)) @ (j /\ k)).1, (i = 1) -> <k> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ k)).1, (j = 0) -> <k> cC.1.1 ])) cC.1.2 [ (i = 0) -> <j> (cC.2 ((x,z)) @ j).2, (i = 1) -> <j> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ j).2 ]) [ (i = 0) -> <j> z, (i = 1) -> <j> f (comp (<k> A) cC.1.1 [ (j = 0) -> <k> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ k).1, (j = 1) -> <k> (cC.2 ((x,z)) @ k).1 ]) (comp (<k> B (comp (<i> A) cC.1.1 [ (j = 0) -> <i> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1, (j = 1)(k = 1) -> <i> (cC.2 ((x,z)) @ i).1, (k = 0) -> <i> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1 ])) cB.1.2 [ (j = 0) -> <k> cB.1.2 ]) ]),\(x0 : sig (B x) (\(x0 : B x) -> IdP (<i> C x) z (f x x0))) -> <i> (comp (<j> B x) (comp (<j> B (comp (<k> A) cC.1.1 [ (i = 0) -> <k> comp (<l> A) cC.1.1 [ (j = 0) -> <l> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (k /\ l)).1, (j = 1) -> <l> (cC.2 ((x,z)) @ (k /\ l)).1, (k = 0) -> <l> cC.1.1 ], (i = 1) -> <k> (cC.2 ((x,x0.2 @ -j)) @ k).1, (j = 0) -> <k> (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) -> <k> (cC.2 ((x,z)) @ k).1 ])) (cB.2 ((x,x0.1)) @ i).2 []) [ (i = 0) -> <j> comp (<i> B (comp (<k> A) cC.1.1 [ (i = 0) -> <k> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ k).1, (i = 1) -> <k> (cC.2 ((x,z)) @ k).1 ])) cB.1.2 [], (i = 1) -> <j> comp (<k> B x) x0.1 [ (j = 1) -> <k> x0.1 ] ],<k> comp (<l> C x) (comp (<l> C (comp (<j> A) cC.1.1 [ (i = 0) -> <j> comp (<m> A) cC.1.1 [ (j = 0) -> <m> cC.1.1, (k = 0) -> <m> (cC.2 ((x,z)) @ (j /\ m)).1, (k = 1)(l = 0) -> <m> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ m)).1, (l = 1) -> <m> (cC.2 ((x,z)) @ (j /\ m)).1 ], (i = 1) -> <j> (cC.2 ((x,x0.2 @ (-l /\ k))) @ j).1, (k = 0) -> <j> (cC.2 ((x,z)) @ j).1, (k = 1)(l = 0) -> <j> (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) -> <j> (cC.2 ((x,z)) @ j).1 ])) (comp (<l> C (comp (<j> A) cC.1.1 [ (i = 0) -> <j> comp (<m> A) cC.1.1 [ (j = 0) -> <m> cC.1.1, (k = 0) -> <m> (cC.2 ((x,z)) @ (l /\ j /\ m)).1, (k = 1) -> <m> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (l /\ j /\ m)).1, (l = 0) -> <m> cC.1.1 ], (i = 1) -> <j> (cC.2 ((x,x0.2 @ k)) @ (l /\ j)).1, (k = 0) -> <j> (cC.2 ((x,z)) @ (l /\ j)).1, (k = 1) -> <j> (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) -> <j> cC.1.1 ])) cC.1.2 [ (i = 0) -> <l> comp (<j> C (comp (<m> A) cC.1.1 [ (j = 0) -> <m> cC.1.1, (k = 0) -> <m> (cC.2 ((x,z)) @ (l /\ j /\ m)).1, (k = 1) -> <m> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (l /\ j /\ m)).1, (l = 0) -> <m> cC.1.1 ])) cC.1.2 [ (k = 0) -> <j> (cC.2 ((x,z)) @ (l /\ j)).2, (k = 1) -> <j> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (l /\ j)).2, (l = 0) -> <j> cC.1.2 ], (i = 1) -> <l> (cC.2 ((x,x0.2 @ k)) @ l).2, (k = 0) -> <l> (cC.2 ((x,z)) @ l).2, (k = 1) -> <l> (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) -> <l> z, (k = 1) -> <l> f (comp (<k> A) cC.1.1 [ (i = 0) -> <k> comp (<j> A) cC.1.1 [ (k = 0) -> <j> cC.1.1, (l = 0) -> <j> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (k /\ j)).1, (l = 1) -> <j> (cC.2 ((x,z)) @ (k /\ j)).1 ], (i = 1) -> <k> (cC.2 ((x,x0.2 @ -l)) @ k).1, (l = 0) -> <k> (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) -> <k> (cC.2 ((x,z)) @ k).1 ]) (comp (<k> B (comp (<j> A) cC.1.1 [ (i = 0) -> <j> comp (<m> A) cC.1.1 [ (j = 0) -> <m> cC.1.1, (k = 0) -> <m> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ m)).1, (k = 1)(l = 1) -> <m> (cC.2 ((x,z)) @ (j /\ m)).1, (l = 0) -> <m> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ m)).1 ], (i = 1) -> <j> (cC.2 ((x,x0.2 @ (-l \/ -k))) @ j).1, (k = 0) -> <j> (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) -> <j> (cC.2 ((x,z)) @ j).1, (l = 0) -> <j> (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) -> <k> (cB.2 ((x,x0.1)) @ i).2 ]) ]) [ (i = 0) -> <l> comp (<j> C (comp (<i> A) cC.1.1 [ (j = 0)(k = 1) -> <i> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1, (j = 1) -> <i> (cC.2 ((x,z)) @ i).1, (k = 0) -> <i> (cC.2 ((x,z)) @ i).1 ])) (comp (<j> C (comp (<i> A) cC.1.1 [ (j = 0) -> <i> cC.1.1, (k = 0) -> <i> (cC.2 ((x,z)) @ (j /\ i)).1, (k = 1) -> <i> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ i)).1 ])) cC.1.2 [ (k = 0) -> <j> (cC.2 ((x,z)) @ j).2, (k = 1) -> <j> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ j).2 ]) [ (k = 0) -> <j> z, (k = 1) -> <j> f (comp (<l> A) cC.1.1 [ (j = 0) -> <l> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ l).1, (j = 1) -> <l> (cC.2 ((x,z)) @ l).1 ]) (comp (<l> B (comp (<i> A) cC.1.1 [ (j = 0) -> <i> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1, (j = 1)(l = 1) -> <i> (cC.2 ((x,z)) @ i).1, (l = 0) -> <i> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1 ])) cB.1.2 [ (j = 0) -> <l> cB.1.2 ]) ], (i = 1) -> <l> comp (<j> C x) (x0.2 @ k) [ (k = 0) -> <j> z, (k = 1) -> <j> f x (comp (<k> B x) x0.1 [ (j = 0) -> <k> x0.1, (l = 1) -> <k> x0.1 ]), (l = 1) -> <j> x0.2 @ k ], (k = 0) -> <l> z, (k = 1) -> <l> f x (comp (<k> B x) (comp (<l> B (comp (<k> A) cC.1.1 [ (i = 0) -> <k> comp (<j> A) cC.1.1 [ (k = 0) -> <j> cC.1.1, (l = 0) -> <j> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (k /\ j)).1, (l = 1) -> <j> (cC.2 ((x,z)) @ (k /\ j)).1 ], (i = 1) -> <k> (cC.2 ((x,x0.2 @ -l)) @ k).1, (l = 0) -> <k> (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) -> <k> (cC.2 ((x,z)) @ k).1 ])) (cB.2 ((x,x0.1)) @ i).2 []) [ (i = 0) -> <k> comp (<i> B (comp (<k> A) cC.1.1 [ (i = 0) -> <k> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ k).1, (i = 1) -> <k> (cC.2 ((x,z)) @ k).1 ])) cB.1.2 [], (i = 1) -> <k> comp (<j> B x) x0.1 [ (k = 1)(l = 1) -> <j> x0.1 ], (l = 0) -> <k> comp (<l> B (comp (<k> A) cC.1.1 [ (i = 0) -> <k> comp (<j> A) cC.1.1 [ (k = 0) -> <j> cC.1.1, (l = 0) -> <j> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (k /\ j)).1, (l = 1) -> <j> (cC.2 ((x,z)) @ (k /\ j)).1 ], (i = 1) -> <k> (cC.2 ((x,x0.2 @ -l)) @ k).1, (l = 0) -> <k> (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) -> <k> (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)
- -> <i> 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
- = <j> (glueElem (comp (<_> B) b [(i=0) -> <k> 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) -> <l> 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) = <i> (p @ -i,<j> 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 (<i>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) (<i>corrUniv A A@-i) (idEquiv A)
-
--- obtained by normal form
-
-testUniv1 (A:U) : Id U A A =
- <i> comp (<_>U)
- (comp (<_>U) A
- [ (i = 0) -> <l> comp (<_>U) A [ (l = 0) -> <i> glue A [ (i = 0) -> (A,(\(x : A) -> x,\(a : A) -> ((a,<l> a),\(z : ((x : A) * IdP (<l> A) a x)) -> <l> (z.2 @ l,<i> z.2 @ (l /\ i))))), (i = 1) -> (A,(comp (<l> A -> A) (\(x : A) -> x) [],comp (<l> (y : A) ->
- ((x : ((x : A) * IdP (<j> A) y (comp (<j> A) (comp (<i> A) x []) [ (l = 0) -> <j> comp (<k> A) x [ (j = 1) -> <k> x ] ]))) * (y0 : ((x0 : A) * IdP (<j> A) y (comp (<j> A) (comp (<i> A) x0 []) [ (l = 0) -> <j> comp (<k> A) x0 [ (j = 1) -> <k> x0 ] ]))) -> IdP (<j> ((x0 : A) * IdP (<j> A) y (comp (<j> A) (comp (<i> A) x0 []) [ (l = 0) -> <j> comp (<k> A) x0 [ (j = 1) -> <k> x0 ] ]))) x y0)) (\(a : A) -> ((a,<l> a),\(z : ((x : A) * IdP (<l> A) a x)) -> <l> (z.2 @ l,<i> z.2 @ (l /\ i)))) [])) ], (l = 1) -> <i> glue A [ (i = 0) -> (A,(\(x : A) -> x,\(a : A) -> ((a,<l> a),\(z : ((x : A) * IdP (<l> A) a x)) -> <l> (z.2 @ l,<i> z.2 @ (l /\ i))))), (i = 1) -> (A,(comp (<l> A -> A) (\(x : A) -> x) [],comp (<l> (y : A) ->
- ((x : ((x : A) * IdP (<j> A) y (comp (<j> A) (comp (<i> A) x []) [ (l = 0) -> <j> comp (<k> A) x [ (j = 1) -> <k> x ] ]))) * (y0 : ((x0 : A) * IdP (<j> A) y (comp (<j> A) (comp (<i> A) x0 []) [ (l = 0) -> <j> comp (<k> A) x0 [ (j = 1) -> <k> x0 ] ]))) -> IdP (<j> ((x0 : A) * IdP (<j> A) y (comp (<j> A) (comp (<i> A) x0 []) [ (l = 0) -> <j> comp (<k> A) x0 [ (j = 1) -> <k> x0 ] ]))) x y0)) (\(a : A) -> ((a,<l> a),\(z : ((x : A) * IdP (<l> A) a x)) -> <l> (z.2 @ l,<i> z.2 @ (l /\ i)))) [])) ] ], (i = 1) -> <l> A ]) [ (i = 0) -> <l> A, (i = 1) -> <l> A ]
-
-data bool = true | false
-
-testUniv2 : bool = trans bool bool (testUniv1 bool) true
-
-testUniv2 : bool =
- comp (<i> comp (<_>U) (comp (<_>U) bool [ (i = 0) -> <j> comp (<_>U) bool [ (j = 0) -> <i> glue bool [ (i = 0) -> (bool,(\(x : bool) -> x,\(a : bool) -> ((a,<i> a),\(z : ((x : bool) * IdP (<i> bool) a x)) -> <i> (z.2 @ i,<j> z.2 @ (i /\ j))))), (i = 1) -> (bool,(comp (<i> bool -> bool) (\(x : bool) -> x) [],comp (<i> (y : bool) ->
- ((x : ((x : bool) * IdP (<j> bool) y (comp (<j> bool) (comp (<i> bool) x []) [ (i = 0) -> <j> comp (<k> bool) x [ (j = 1) -> <k> x ] ]))) * (y0 : ((x0 : bool) * IdP (<j> bool) y (comp (<j> bool) (comp (<i> bool) x0 []) [ (i = 0) -> <j> comp (<k> bool) x0 [ (j = 1) -> <k> x0 ] ]))) -> IdP (<j> ((x0 : bool) * IdP (<k> bool) y (comp (<j> bool) (comp (<i> bool) x0 []) [ (i = 0) -> <j> comp (<k> bool) x0 [ (j = 1) -> <k> x0 ] ]))) x y0)) (\(a : bool) -> ((a,<i> a),\(z : ((x : bool) * IdP (<i> bool) a x)) -> <i> (z.2 @ i,<j> z.2 @ (i /\ j)))) [])) ], (j = 1) -> <i> glue bool [ (i = 0) -> (bool,(\(x : bool) -> x,\(a : bool) -> ((a,<i> a),\(z : ((x : bool) * IdP (<i> bool) a x)) -> <i> (z.2 @ i,<j> z.2 @ (i /\ j))))), (i = 1) -> (bool,(comp (<i> bool -> bool) (\(x : bool) -> x) [],comp (<i> (y : bool) ->
- ((x : ((x : bool) * IdP (<j> bool) y (comp (<j> bool) (comp (<i> bool) x []) [ (i = 0) -> <j> comp (<k> bool) x [ (j = 1) -> <k> x ] ]))) * (y0 : ((x0 : bool) * IdP (<j> bool) y (comp (<j> bool) (comp (<i> bool) x0 []) [ (i = 0) -> <j> comp (<k> bool) x0 [ (j = 1) -> <k> x0 ] ]))) -> IdP (<j> ((x0 : bool) * IdP (<k> bool) y (comp (<j> bool) (comp (<i> bool) x0 []) [ (i = 0) -> <j> comp (<k> bool) x0 [ (j = 1) -> <k> x0 ] ]))) x y0)) (\(a : bool) -> ((a,<i> a),\(z : ((x : bool) * IdP (<i> bool) a x)) -> <i> (z.2 @ i,<j> z.2 @ (i /\ j)))) [])) ] ], (i = 1) -> <j> bool ]) [ (i = 0) -> <j> bool, (i = 1) -> <j> 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)
--- /dev/null
+-- 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 = <i>comp (<j>A) (g (q (f x)@i)) [(i=0) -> <j>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 =
+ <i>(p z.1@i,h (p z.1@i) (comp (<j>B (p z.1@i\/-j)) z.2 [(i=1)-><j>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 = <i>comp (<j>A) a [(i=0) -> f x,(i=1) -> f y]
+ q (p:Id A x y) : Id (Id A x y) p0 p =
+ <j i>comp (<k>A) a [(i=0) -> f x,(i=1) -> f y,
+ (j=0) -> <k>comp (<l>A) a [(k=0) -> <l>a,(i=0) -> <l>f x@k/\l,(i=1) -> <l>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),<i>(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 = <i>(w.2@i).1
+ q : IdP (<i>C (p@i)) z0 (f x b) = <i>(w.2@i).2
+ b0 : B x0 = comp (<i>B (p@-i)) b []
+ r : IdP (<i>B (p@-i)) b b0 = <i>comp (<j>B (p@-j\/-i)) b [(i=0) -> <k>b]
+ s : Id (C x0) z0 (f x0 b0) = <i>comp (<j>C (p@(i/\-j))) (q@i) [(i=0) -> <k>z0,(i=1) -> <k>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 =
+ <l> (comp (<i> B x0) u.1 [(l=1) -> <j>u.1],
+ <i> comp (<j> C x0) (u.2 @ i) [ (l=1) -> <j> u.2 @ i,
+ (i = 0) -> <j> z0,
+ (i = 1) -> <j> f x0 (comp (<k> B x0) u.1 [ (j = 0) -> <k> u.1, (l=1) -> <k>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 (<i> B (comp (<j> A) cC.1.1 [ (i = 0) -> <j> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ j).1, (i = 1) -> <j> (cC.2 ((x,z)) @ j).1 ])) cB.1.2 [],<i> comp (<j> C (comp (<k> A) cC.1.1 [ (i = 0) -> <k> (cC.2 ((x,z)) @ k).1, (i = 1)(j = 0) -> <k> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ k).1, (j = 1) -> <k> (cC.2 ((x,z)) @ k).1 ])) (comp (<j> C (comp (<k> A) cC.1.1 [ (i = 0) -> <k> (cC.2 ((x,z)) @ (j /\ k)).1, (i = 1) -> <k> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ k)).1, (j = 0) -> <k> cC.1.1 ])) cC.1.2 [ (i = 0) -> <j> (cC.2 ((x,z)) @ j).2, (i = 1) -> <j> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ j).2 ]) [ (i = 0) -> <j> z, (i = 1) -> <j> f (comp (<k> A) cC.1.1 [ (j = 0) -> <k> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ k).1, (j = 1) -> <k> (cC.2 ((x,z)) @ k).1 ]) (comp (<k> B (comp (<i> A) cC.1.1 [ (j = 0) -> <i> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1, (j = 1)(k = 1) -> <i> (cC.2 ((x,z)) @ i).1, (k = 0) -> <i> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1 ])) cB.1.2 [ (j = 0) -> <k> cB.1.2 ]) ]),\(x0 : sig (B x) (\(x0 : B x) -> IdP (<i> C x) z (f x x0))) -> <i> (comp (<j> B x) (comp (<j> B (comp (<k> A) cC.1.1 [ (i = 0) -> <k> comp (<l> A) cC.1.1 [ (j = 0) -> <l> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (k /\ l)).1, (j = 1) -> <l> (cC.2 ((x,z)) @ (k /\ l)).1, (k = 0) -> <l> cC.1.1 ], (i = 1) -> <k> (cC.2 ((x,x0.2 @ -j)) @ k).1, (j = 0) -> <k> (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) -> <k> (cC.2 ((x,z)) @ k).1 ])) (cB.2 ((x,x0.1)) @ i).2 []) [ (i = 0) -> <j> comp (<i> B (comp (<k> A) cC.1.1 [ (i = 0) -> <k> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ k).1, (i = 1) -> <k> (cC.2 ((x,z)) @ k).1 ])) cB.1.2 [], (i = 1) -> <j> comp (<k> B x) x0.1 [ (j = 1) -> <k> x0.1 ] ],<k> comp (<l> C x) (comp (<l> C (comp (<j> A) cC.1.1 [ (i = 0) -> <j> comp (<m> A) cC.1.1 [ (j = 0) -> <m> cC.1.1, (k = 0) -> <m> (cC.2 ((x,z)) @ (j /\ m)).1, (k = 1)(l = 0) -> <m> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ m)).1, (l = 1) -> <m> (cC.2 ((x,z)) @ (j /\ m)).1 ], (i = 1) -> <j> (cC.2 ((x,x0.2 @ (-l /\ k))) @ j).1, (k = 0) -> <j> (cC.2 ((x,z)) @ j).1, (k = 1)(l = 0) -> <j> (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) -> <j> (cC.2 ((x,z)) @ j).1 ])) (comp (<l> C (comp (<j> A) cC.1.1 [ (i = 0) -> <j> comp (<m> A) cC.1.1 [ (j = 0) -> <m> cC.1.1, (k = 0) -> <m> (cC.2 ((x,z)) @ (l /\ j /\ m)).1, (k = 1) -> <m> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (l /\ j /\ m)).1, (l = 0) -> <m> cC.1.1 ], (i = 1) -> <j> (cC.2 ((x,x0.2 @ k)) @ (l /\ j)).1, (k = 0) -> <j> (cC.2 ((x,z)) @ (l /\ j)).1, (k = 1) -> <j> (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) -> <j> cC.1.1 ])) cC.1.2 [ (i = 0) -> <l> comp (<j> C (comp (<m> A) cC.1.1 [ (j = 0) -> <m> cC.1.1, (k = 0) -> <m> (cC.2 ((x,z)) @ (l /\ j /\ m)).1, (k = 1) -> <m> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (l /\ j /\ m)).1, (l = 0) -> <m> cC.1.1 ])) cC.1.2 [ (k = 0) -> <j> (cC.2 ((x,z)) @ (l /\ j)).2, (k = 1) -> <j> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (l /\ j)).2, (l = 0) -> <j> cC.1.2 ], (i = 1) -> <l> (cC.2 ((x,x0.2 @ k)) @ l).2, (k = 0) -> <l> (cC.2 ((x,z)) @ l).2, (k = 1) -> <l> (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) -> <l> z, (k = 1) -> <l> f (comp (<k> A) cC.1.1 [ (i = 0) -> <k> comp (<j> A) cC.1.1 [ (k = 0) -> <j> cC.1.1, (l = 0) -> <j> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (k /\ j)).1, (l = 1) -> <j> (cC.2 ((x,z)) @ (k /\ j)).1 ], (i = 1) -> <k> (cC.2 ((x,x0.2 @ -l)) @ k).1, (l = 0) -> <k> (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) -> <k> (cC.2 ((x,z)) @ k).1 ]) (comp (<k> B (comp (<j> A) cC.1.1 [ (i = 0) -> <j> comp (<m> A) cC.1.1 [ (j = 0) -> <m> cC.1.1, (k = 0) -> <m> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ m)).1, (k = 1)(l = 1) -> <m> (cC.2 ((x,z)) @ (j /\ m)).1, (l = 0) -> <m> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ m)).1 ], (i = 1) -> <j> (cC.2 ((x,x0.2 @ (-l \/ -k))) @ j).1, (k = 0) -> <j> (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) -> <j> (cC.2 ((x,z)) @ j).1, (l = 0) -> <j> (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) -> <k> (cB.2 ((x,x0.1)) @ i).2 ]) ]) [ (i = 0) -> <l> comp (<j> C (comp (<i> A) cC.1.1 [ (j = 0)(k = 1) -> <i> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1, (j = 1) -> <i> (cC.2 ((x,z)) @ i).1, (k = 0) -> <i> (cC.2 ((x,z)) @ i).1 ])) (comp (<j> C (comp (<i> A) cC.1.1 [ (j = 0) -> <i> cC.1.1, (k = 0) -> <i> (cC.2 ((x,z)) @ (j /\ i)).1, (k = 1) -> <i> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ i)).1 ])) cC.1.2 [ (k = 0) -> <j> (cC.2 ((x,z)) @ j).2, (k = 1) -> <j> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ j).2 ]) [ (k = 0) -> <j> z, (k = 1) -> <j> f (comp (<l> A) cC.1.1 [ (j = 0) -> <l> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ l).1, (j = 1) -> <l> (cC.2 ((x,z)) @ l).1 ]) (comp (<l> B (comp (<i> A) cC.1.1 [ (j = 0) -> <i> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1, (j = 1)(l = 1) -> <i> (cC.2 ((x,z)) @ i).1, (l = 0) -> <i> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1 ])) cB.1.2 [ (j = 0) -> <l> cB.1.2 ]) ], (i = 1) -> <l> comp (<j> C x) (x0.2 @ k) [ (k = 0) -> <j> z, (k = 1) -> <j> f x (comp (<k> B x) x0.1 [ (j = 0) -> <k> x0.1, (l = 1) -> <k> x0.1 ]), (l = 1) -> <j> x0.2 @ k ], (k = 0) -> <l> z, (k = 1) -> <l> f x (comp (<k> B x) (comp (<l> B (comp (<k> A) cC.1.1 [ (i = 0) -> <k> comp (<j> A) cC.1.1 [ (k = 0) -> <j> cC.1.1, (l = 0) -> <j> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (k /\ j)).1, (l = 1) -> <j> (cC.2 ((x,z)) @ (k /\ j)).1 ], (i = 1) -> <k> (cC.2 ((x,x0.2 @ -l)) @ k).1, (l = 0) -> <k> (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) -> <k> (cC.2 ((x,z)) @ k).1 ])) (cB.2 ((x,x0.1)) @ i).2 []) [ (i = 0) -> <k> comp (<i> B (comp (<k> A) cC.1.1 [ (i = 0) -> <k> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ k).1, (i = 1) -> <k> (cC.2 ((x,z)) @ k).1 ])) cB.1.2 [], (i = 1) -> <k> comp (<j> B x) x0.1 [ (k = 1)(l = 1) -> <j> x0.1 ], (l = 0) -> <k> comp (<l> B (comp (<k> A) cC.1.1 [ (i = 0) -> <k> comp (<j> A) cC.1.1 [ (k = 0) -> <j> cC.1.1, (l = 0) -> <j> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (k /\ j)).1, (l = 1) -> <j> (cC.2 ((x,z)) @ (k /\ j)).1 ], (i = 1) -> <k> (cC.2 ((x,x0.2 @ -l)) @ k).1, (l = 0) -> <k> (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) -> <k> (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)
+ -> <i> 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
+ = <j> (glueElem (comp (<_> B) b [(i=0) -> <k> 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) -> <l> 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) = <i> (p @ -i,<j> 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 (<i>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) (<i> corrUniv A A @ -i) (idEquiv A)
+
+-- obtained by normal form
+ntestUniv1 (A:U) : Id U A A =
+ <i> comp (<_>U)
+ (comp (<_>U) A
+ [ (i = 0) -> <l> comp (<_>U) A [ (l = 0) -> <i> glue A [ (i = 0) -> (A,(\(x : A) -> x,\(a : A) -> ((a,<l> a),\(z : ((x : A) * IdP (<l> A) a x)) -> <l> (z.2 @ l,<i> z.2 @ (l /\ i))))), (i = 1) -> (A,(comp (<l> A -> A) (\(x : A) -> x) [],comp (<l> (y : A) ->
+ ((x : ((x : A) * IdP (<j> A) y (comp (<j> A) (comp (<i> A) x []) [ (l = 0) -> <j> comp (<k> A) x [ (j = 1) -> <k> x ] ]))) * (y0 : ((x0 : A) * IdP (<j> A) y (comp (<j> A) (comp (<i> A) x0 []) [ (l = 0) -> <j> comp (<k> A) x0 [ (j = 1) -> <k> x0 ] ]))) -> IdP (<j> ((x0 : A) * IdP (<j> A) y (comp (<j> A) (comp (<i> A) x0 []) [ (l = 0) -> <j> comp (<k> A) x0 [ (j = 1) -> <k> x0 ] ]))) x y0)) (\(a : A) -> ((a,<l> a),\(z : ((x : A) * IdP (<l> A) a x)) -> <l> (z.2 @ l,<i> z.2 @ (l /\ i)))) [])) ], (l = 1) -> <i> glue A [ (i = 0) -> (A,(\(x : A) -> x,\(a : A) -> ((a,<l> a),\(z : ((x : A) * IdP (<l> A) a x)) -> <l> (z.2 @ l,<i> z.2 @ (l /\ i))))), (i = 1) -> (A,(comp (<l> A -> A) (\(x : A) -> x) [],comp (<l> (y : A) ->
+ ((x : ((x : A) * IdP (<j> A) y (comp (<j> A) (comp (<i> A) x []) [ (l = 0) -> <j> comp (<k> A) x [ (j = 1) -> <k> x ] ]))) * (y0 : ((x0 : A) * IdP (<j> A) y (comp (<j> A) (comp (<i> A) x0 []) [ (l = 0) -> <j> comp (<k> A) x0 [ (j = 1) -> <k> x0 ] ]))) -> IdP (<j> ((x0 : A) * IdP (<j> A) y (comp (<j> A) (comp (<i> A) x0 []) [ (l = 0) -> <j> comp (<k> A) x0 [ (j = 1) -> <k> x0 ] ]))) x y0)) (\(a : A) -> ((a,<l> a),\(z : ((x : A) * IdP (<l> A) a x)) -> <l> (z.2 @ l,<i> z.2 @ (l /\ i)))) [])) ] ], (i = 1) -> <l> A ]) [ (i = 0) -> <l> A, (i = 1) -> <l> A ]
+
+testUniv2 : bool = trans bool bool (testUniv1 bool) true
+
+ntestUniv2 : bool =
+ comp (<i> comp (<_>U) (comp (<_>U) bool [ (i = 0) -> <j> comp (<_>U) bool [ (j = 0) -> <i> glue bool [ (i = 0) -> (bool,(\(x : bool) -> x,\(a : bool) -> ((a,<i> a),\(z : ((x : bool) * IdP (<i> bool) a x)) -> <i> (z.2 @ i,<j> z.2 @ (i /\ j))))), (i = 1) -> (bool,(comp (<i> bool -> bool) (\(x : bool) -> x) [],comp (<i> (y : bool) ->
+ ((x : ((x : bool) * IdP (<j> bool) y (comp (<j> bool) (comp (<i> bool) x []) [ (i = 0) -> <j> comp (<k> bool) x [ (j = 1) -> <k> x ] ]))) * (y0 : ((x0 : bool) * IdP (<j> bool) y (comp (<j> bool) (comp (<i> bool) x0 []) [ (i = 0) -> <j> comp (<k> bool) x0 [ (j = 1) -> <k> x0 ] ]))) -> IdP (<j> ((x0 : bool) * IdP (<k> bool) y (comp (<j> bool) (comp (<i> bool) x0 []) [ (i = 0) -> <j> comp (<k> bool) x0 [ (j = 1) -> <k> x0 ] ]))) x y0)) (\(a : bool) -> ((a,<i> a),\(z : ((x : bool) * IdP (<i> bool) a x)) -> <i> (z.2 @ i,<j> z.2 @ (i /\ j)))) [])) ], (j = 1) -> <i> glue bool [ (i = 0) -> (bool,(\(x : bool) -> x,\(a : bool) -> ((a,<i> a),\(z : ((x : bool) * IdP (<i> bool) a x)) -> <i> (z.2 @ i,<j> z.2 @ (i /\ j))))), (i = 1) -> (bool,(comp (<i> bool -> bool) (\(x : bool) -> x) [],comp (<i> (y : bool) ->
+ ((x : ((x : bool) * IdP (<j> bool) y (comp (<j> bool) (comp (<i> bool) x []) [ (i = 0) -> <j> comp (<k> bool) x [ (j = 1) -> <k> x ] ]))) * (y0 : ((x0 : bool) * IdP (<j> bool) y (comp (<j> bool) (comp (<i> bool) x0 []) [ (i = 0) -> <j> comp (<k> bool) x0 [ (j = 1) -> <k> x0 ] ]))) -> IdP (<j> ((x0 : bool) * IdP (<k> bool) y (comp (<j> bool) (comp (<i> bool) x0 []) [ (i = 0) -> <j> comp (<k> bool) x0 [ (j = 1) -> <k> x0 ] ]))) x y0)) (\(a : bool) -> ((a,<i> a),\(z : ((x : bool) * IdP (<i> bool) a x)) -> <i> (z.2 @ i,<j> z.2 @ (i /\ j)))) [])) ] ], (i = 1) -> <j> bool ]) [ (i = 0) -> <j> bool, (i = 1) -> <j> 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) =
+-- <i> fill (<_> A -> A) (idfun A) [] @ -i
+
+-- transDiagTrans (A : U) : Id (A -> A) (idfun A) (trans A A (<_> A)) =
+-- <i> \ (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) =
+-- <i> \ (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
projects / cubicaltt.git / commitdiff