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)
++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))
++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
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 =
++ 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)
++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 =
++ 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)]
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 =
++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
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)
++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
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) :
++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) :
++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 = 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)
++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)
(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)
++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)
- lem1 (A:U) : isContr ((X:U) * equiv A X) = undefined
+ idEquiv (A:U) : equiv A A = (\ (x:A) -> x, lemSinglContr A)
+
-lem1 (B:U) : isContr ((X:U) * equiv X B) =
++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) =
++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> 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)))) [])) ], (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) ->
++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 (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)
- 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)
--- thmUniv (lem1 : (A:U) -> isContr ((X:U) * equiv A X)) (t : (A X:U) -> Id U A X -> equiv A X) (A:U)
++-- 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)
--module testEquiv where\r
--\r
--import prelude\r
--\r
--fiber (A B : U) (f : A -> B) (y : B) : U =\r
-- (x : A) * Id B y (f x)\r
--\r
--isContr (A:U) : U = (a:A) * ((x:A) -> Id A a x)\r
--\r
--propIsContr (A:U) (z0 z1:isContr A) : Id (isContr A) z0 z1 =\r
-- <j>(p0 a1@j,\r
-- \ (x:A) -> \r
-- <i>comp (<_>A) (lem1 x@i@j) [ (i=0) -> <k>p0 a1@j, (i=1) -> <k>p0 x@(j\/k),\r
-- (j=0) -> <k>p0 x@(i/\k), (j=1) -> <k>p1 x@i ])\r
-- where\r
-- a0 : A = z0.1\r
-- p0 : (x:A) -> Id A a0 x = z0.2\r
-- a1 : A = z1.1\r
-- p1 : (x:A) -> Id A a1 x = z1.2\r
-- lem1 (x:A) : IdP (<i>Id A a0 (p1 x@i)) (p0 a1) (p0 x) = <i j> p0 (p1 x@i) @ j\r
-- \r
--isEquiv (A B : U) (f : A -> B) : U = (y:B) -> isContr (fiber A B f y)\r
--\r
--equiv (A B : U) : U = (f : A -> B) * isEquiv A B f\r
--\r
--propIsEquiv (A B : U) (f : A -> B)\r
-- : 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\r
--\r
--lemPropF (A : U) (P : A -> U) (pP : (x : A) -> prop (P x)) (a0 a1 :A) \r
-- (p : Id A a0 a1) (b0 : P a0) (b1 : P a1) : IdP (<i>P (p@i)) b0 b1 =\r
-- <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\r
--\r
--lemSig (A : U) (B : A -> U) (pB : (x : A) -> prop (B x))\r
-- (u v : (x:A) * B x) (p : Id A u.1 v.1) :\r
-- Id ((x:A) * B x) u v =\r
-- <i> (p@i,(lemPropF A B pB u.1 v.1 p u.2 v.2)@i)\r
--\r
--propSig (A : U) (B : A -> U) (pA : prop A)\r
-- (pB : (x : A) -> prop (B x)) (t u : (x:A) * B x) :\r
-- Id ((x:A) * B x) t u =\r
-- lemSig A B pB t u (pA t.1 u.1)\r
--\r
--equivLemma (A B : U)\r
-- : (v w : equiv A B) -> Id (A -> B) v.1 w.1 -> Id (equiv A B) v w\r
-- = lemSig (A -> B) (isEquiv A B) (propIsEquiv A B)\r
--\r
---- for univalence\r
--\r
--invEq (A B:U) (w:equiv A B) (y:B) : A = (w.2 y).1.1\r
--\r
--retEq (A B:U) (w:equiv A B) (y:B) : Id B (w.1 (invEq A B w y)) y =\r
-- <i>(w.2 y).1.2@-i\r
--\r
--secEq (A B:U) (w:equiv A B) (x:A) : Id A (invEq A B w (w.1 x)) x =\r
-- <i> ((w.2 (w.1 x)).2 (x,<j>w.1 x)@i).1\r
--\r
---- transDelta (A:U) : equiv A A = \r
--\r
--transEquiv (A B:U) (p:Id U A B) : equiv A B = (f,p)\r
-- where\r
-- f (x:A) : B = comp p x []\r
-- g (y:B) : A = comp (<i>p@-i) y []\r
-- lem1 (x:A) : IdP p x (f x) = <i>comp (<j>p@(i/\j)) x [(i=0) -> <j>x]\r
-- lem2 (y:B) : IdP p (g y) y = <i>comp (<j>p@(i\/-j)) y [(i=1) -> <j>y]\r
-- lem3 (y:B) : Id B y (f (g y)) = <i>comp p (g y) [(i=0) -> lem2 y,(i=1) -> lem1 (g y)]\r
-- lem4 (y:B) : IdP (<i>Id (p@i) (lem2 y@i) (lem1 (g y)@i)) (<j>g y) (lem3 y) =\r
-- <j i>fill p (g y) [(i=0) -> lem2 y,(i=1) -> lem1 (g y)] @ j\r
-- lem5 (y:B) (x:A) (q:Id B y (f x)) : Id A (g y) x = \r
-- <i>comp (<j>p@-j) (q@i) [(i=0) -> <j>lem2 y@-j,(i=1) -> <j>lem1 x@-j]\r
-- lem6 (y:B) (x:A) (q:Id B y (f x)) : IdP (<i>Id (p@i) (lem2 y@i) (lem1 x@i)) (lem5 y x q) q =\r
-- <j i>fill (<j>p@-j) (q@i) [(i=0) -> <k>lem2 y@-k,(i=1) -> <k>lem1 x@-k] @ -j\r
-- lem7 (y:B) (x:A) (q:Id B y (f x)) : IdP (<i>Id B y (f (lem5 y x q@i))) (lem3 y) q = \r
-- <j i>comp p (lem5 y x q@i/\j) [(i=0) -> lem2 y, (i=1) -> lem1 (lem5 y x q@j),(j=0) -> <k>lem4 y@k@i,(j=1) -> <k>lem6 y x q@k@i]\r
-- lem8 (y:B) : fiber A B f y = (g y,lem3 y)\r
-- lem9 (y:B) (z:fiber A B f y) : Id (fiber A B f y) (lem8 y) z =\r
-- <i>(lem5 y z.1 z.2@i,lem7 y z.1 z.2@i)\r
-- p (y:B) : isContr (fiber A B f y) = (lem8 y,lem9 y)\r
-\r
-lemSinglContr (A:U) (a:A) : isContr ((x:A) * Id A a x) =\r
- ((a,refl A a),\ (z:(x:A) * Id A a x) -> contrSingl A a z.1 z.2)\r
-\r
-idEquiv (A:U) : equiv A A = (\ (x:A) -> x, lemSinglContr A)\r
-\r
-transEquiv (A X:U) (p:Id U A X) : equiv A X = \r
- substTrans U (equiv A) A X p (idEquiv A)\r
--\r
--transDelta (A:U) : equiv A A = transEquiv A A (<i>A)\r
--\r
--transEquivToId (A B : U) (w : equiv A B) : Id U A B =\r
- <i> glue B [ (i = 1) -> (B,eB.1,invEq B B eB,retEq B B eB,secEq B B eB)\r
- , (i = 0) -> (A,w.1,invEq A B w,retEq A B w,secEq A B w) ]\r
- <i> glue B [ (i = 1) -> (B,eB)\r
- , (i = 0) -> (A,w) ]\r
-- where eB : equiv B B = transDelta B\r
--\r
--eqToEq (A B : U) (p : Id U A B)\r
-- : Id (Id U A B) (transEquivToId A B (transEquiv A B p)) p\r
-- = <j i> let e : equiv A B = transEquiv A B p\r
-- f : equiv B B = transDelta B\r
-- Ai : U = p@i\r
-- g : equiv Ai B = transEquiv Ai B (<k> p @ (i \/ k))\r
-- in glue B\r
- [ (i = 0) -> (A,e.1,invEq A B e,retEq A B e,secEq A B e)\r
- , (i = 1) -> (B,f.1,invEq B B f,retEq B B f,secEq B B f)\r
- , (j = 1) -> (p@i,g.1,invEq Ai B g,retEq Ai B g,secEq Ai B g) ]\r
- [ (i = 0) -> (A,e)\r
- , (i = 1) -> (B,f)\r
- , (j = 1) -> (p@i,g)]\r
-\r
-test (A B : U) (w : equiv A B) (x:A) : B = (transEquiv A B (transEquivToId A B w)).1 x\r
--\r
--transIdFun (A B : U) (w : equiv A B)\r
- : Id (A -> B) w.1 (trans A B (transEquivToId A B w)) =\r
- : Id (A -> B) w.1 (transEquiv A B (transEquivToId A B w)).1 =\r
-- <i> \ (a:A) -> \r
-- let b : B = w.1 a\r
- in comp (<j> B) (comp (<j> B) (comp (<j> B) (comp (<j> B) b [(i=0)-><j>b]) [(i=0)-><j>b]) [(i=0)-><j>b]) [(i=0)-><j>b]\r
- u : A = comp (<j>A) a []\r
- q : Id B (w.1 u) b = <i>w.1 (comp (<j>A) a [(i=1) -> <j>a])\r
- in comp (<j> B) \r
- (comp (<j> B) (comp (<j> B) (comp (<j> B) (w.1 u) [(i=0)->q]) [(i=0)-><_>b]) [(i=0)-><_>b]) [(i=0)-><_>b]\r
--\r
--idToId (A B : U) (w : equiv A B)\r
-- : Id (equiv A B) (transEquiv A B (transEquivToId A B w)) w\r
-- = equivLemma A B (transEquiv A B (transEquivToId A B w)) w\r
-- (<i>transIdFun A B w@-i)\r
--\r
--lemIso (A B : U) (f : A -> B) (g : B -> A)\r
-- (s : (y : B) -> Id B (f (g y)) y)\r
-- (t : (x : A) -> Id A (g (f x)) x)\r
-- (y : B) (x0 x1 : A) (p0 : Id B y (f x0)) (p1 : Id B y (f x1)) :\r
-- Id (fiber A B f y) (x0,p0) (x1,p1) = <i> (p @ i,sq1 @ i)\r
-- where\r
-- rem0 : Id A (g y) x0 =\r
-- <i> comp (<_> A) (g (p0 @ i)) [ (i = 1) -> t x0, (i = 0) -> <_> g y ]\r
--\r
-- rem1 : Id A (g y) x1 =\r
-- <i> comp (<_> A) (g (p1 @ i)) [ (i = 1) -> t x1, (i = 0) -> <_> g y ]\r
--\r
-- p : Id A x0 x1 =\r
-- <i> comp (<_> A) (g y) [ (i = 0) -> rem0\r
-- , (i = 1) -> rem1 ]\r
--\r
-- fill0 : Square A (g y) (g (f x0)) (g y) x0\r
-- (<i> g (p0 @ i)) rem0 (<i> g y) (t x0) =\r
-- <i j> comp (<_> A) (g (p0 @ i)) [ (i = 1) -> <k> t x0 @ j /\ k\r
-- , (i = 0) -> <_> g y\r
-- , (j = 0) -> <_> g (p0 @ i) ]\r
--\r
-- fill1 : Square A (g y) (g (f x1)) (g y) x1\r
-- (<i> g (p1 @ i)) rem1 (<i> g y) (t x1) =\r
-- <i j> comp (<_> A) (g (p1 @ i)) [ (i = 1) -> <k> t x1 @ j /\ k\r
-- , (i = 0) -> <_> g y\r
-- , (j = 0) -> <_> g (p1 @ i) ]\r
--\r
-- fill2 : Square A (g y) (g y) x0 x1 \r
-- (<_> g y) p rem0 rem1 =\r
-- <i j> comp (<_> A) (g y) [ (i = 0) -> <k> rem0 @ j /\ k\r
-- , (i = 1) -> <k> rem1 @ j /\ k\r
-- , (j = 0) -> <_> g y ]\r
--\r
-- sq : Square A (g y) (g y) (g (f x0)) (g (f x1)) \r
-- (<i> g y) (<i> g (f (p @ i))) \r
-- (<j> g (p0 @ j)) (<j> g (p1 @ j)) =\r
-- <i j> comp (<_> A) (fill2 @ i @ j) [ (i = 0) -> <k> fill0 @ j @ -k\r
-- , (i = 1) -> <k> fill1 @ j @ -k\r
-- , (j = 0) -> <_> g y\r
-- , (j = 1) -> <k> t (p @ i) @ -k ]\r
--\r
-- sq1 : Square B y y (f x0) (f x1) \r
-- (<_>y) (<i> f (p @ i)) p0 p1 =\r
-- <i j> comp (<_> B) (f (sq @ i @j)) [ (i = 0) -> s (p0 @ j)\r
-- , (i = 1) -> s (p1 @ j)\r
-- , (j = 1) -> s (f (p @ i))\r
-- , (j = 0) -> s y ]\r
--\r
--gradLemma (A B : U) (f : A -> B) (g : B -> A)\r
-- (s : (y : B) -> Id B (f (g y)) y)\r
-- (t : (x : A) -> Id A (g (f x)) x) : isEquiv A B f = \r
-- \ (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)\r
--\r
--transEquivIsEquiv (A B : U)\r
-- : isEquiv (Id U A B) (equiv A B) (transEquiv A B)\r
-- = gradLemma (Id U A B) (equiv A B) (transEquiv A B)\r
-- (transEquivToId A B) (idToId A B) (eqToEq A B)\r
-\r
--\r
--\r
--\r
++module testEquiv where
++
++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 =
++ <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
++
++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 =
++ <i>(w.2 y).1.2@-i
++
++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 []
++ g (y:B) : A = comp (<i>p@-i) y []
++ lem1 (x:A) : IdP p x (f x) = <i>comp (<j>p@(i/\j)) x [(i=0) -> <j>x]
++ lem2 (y:B) : IdP p (g y) y = <i>comp (<j>p@(i\/-j)) y [(i=1) -> <j>y]
++ lem3 (y:B) : Id B y (f (g y)) = <i>comp p (g y) [(i=0) -> lem2 y,(i=1) -> lem1 (g y)]
++ lem4 (y:B) : IdP (<i>Id (p@i) (lem2 y@i) (lem1 (g y)@i)) (<j>g y) (lem3 y) =
++ <j i>fill p (g y) [(i=0) -> lem2 y,(i=1) -> lem1 (g y)] @ j
++ lem5 (y:B) (x:A) (q:Id B y (f x)) : Id A (g y) x =
++ <i>comp (<j>p@-j) (q@i) [(i=0) -> <j>lem2 y@-j,(i=1) -> <j>lem1 x@-j]
++ lem6 (y:B) (x:A) (q:Id B y (f x)) : IdP (<i>Id (p@i) (lem2 y@i) (lem1 x@i)) (lem5 y x q) q =
++ <j i>fill (<j>p@-j) (q@i) [(i=0) -> <k>lem2 y@-k,(i=1) -> <k>lem1 x@-k] @ -j
++ lem7 (y:B) (x:A) (q:Id B y (f x)) : IdP (<i>Id B y (f (lem5 y x q@i))) (lem3 y) q =
++ <j i>comp p (lem5 y x q@i/\j) [(i=0) -> lem2 y, (i=1) -> lem1 (lem5 y x q@j),(j=0) -> <k>lem4 y@k@i,(j=1) -> <k>lem6 y x q@k@i]
++ lem8 (y:B) : fiber A B f y = (g y,lem3 y)
++ lem9 (y:B) (z:fiber A B f y) : Id (fiber A B f y) (lem8 y) z =
++ <i>(lem5 y z.1 z.2@i,lem7 y z.1 z.2@i)
++ p (y:B) : isContr (fiber A B f y) = (lem8 y,lem9 y)
++
++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)
++
++transEquiv (A X:U) (p:Id U A X) : equiv A X =
++ substTrans U (equiv A) A X p (idEquiv A)
++
++transDelta (A:U) : equiv A A = transEquiv A A (<i>A)
++
++transEquivToId (A B : U) (w : equiv A B) : Id U A B =
++ <i> glue B [ (i = 1) -> (B,eB)
++ , (i = 0) -> (A,w) ]
++ where eB : equiv B B = transDelta B
++
++eqToEq (A B : U) (p : Id U A B)
++ : Id (Id U A B) (transEquivToId A B (transEquiv A B p)) p
++ = <j i> let e : equiv A B = transEquiv A B p
++ f : equiv B B = transDelta B
++ Ai : U = p@i
++ g : equiv Ai B = transEquiv Ai B (<k> p @ (i \/ k))
++ in glue B
++ [ (i = 0) -> (A,e)
++ , (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) ->
++ let b : B = w.1 a
++ u : A = comp (<j>A) a []
++ q : Id B (w.1 u) b = <i>w.1 (comp (<j>A) a [(i=1) -> <j>a])
++ in comp (<j> B)
++ (comp (<j> B) (comp (<j> B) (comp (<j> B) (w.1 u) [(i=0)->q]) [(i=0)-><_>b]) [(i=0)-><_>b]) [(i=0)-><_>b]
++
++idToId (A B : U) (w : equiv A B)
++ : Id (equiv A B) (transEquiv A B (transEquivToId A B w)) w
++ = equivLemma A B (transEquiv A B (transEquivToId A B w)) w
++ (<i>transIdFun A B w@-i)
++
++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)
++
++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)
projects / cubicaltt.git / commitdiff