From: Anders Mörtberg <andersmortberg@gmail.com>
Date: Thu, 31 Dec 2015 07:24:29 +0000 (+0100)
Subject: Merge branch 'testUniv'
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=f2a56ccbcdb73e74c756179aa65f0d0524d3bab4;p=cubicaltt.git

Merge branch 'testUniv'

# Conflicts:
#	examples/testContr.ctt
#	examples/testEquiv.ctt
---

f2a56ccbcdb73e74c756179aa65f0d0524d3bab4
diff --cc examples/testContr.ctt
index eda4f1c,95b5022..5bd7bc4
--- a/examples/testContr.ctt
+++ b/examples/testContr.ctt
@@@ -2,14 -2,14 +2,14 @@@ module testContr wher
  
  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
@@@ -17,15 -17,15 +17,15 @@@
    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)]
@@@ -37,7 -37,7 +37,7 @@@ isEquiv (A B : U) (f : A -> B) : U = (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 = 
++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
@@@ -48,8 -48,8 +48,8 @@@ totalFun (A:U) (B C : A->U) (f : (x:A) 
  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
@@@ -59,17 -59,17 +59,17 @@@
    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)
@@@ -77,15 -77,100 +77,99 @@@
                           (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)
diff --cc examples/testEquiv.ctt
index a0155d0,d808c6f..4059918
--- a/examples/testEquiv.ctt
+++ b/examples/testEquiv.ctt
@@@ -1,168 -1,182 +1,178 @@@
--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.1,invEq B B eB,retEq B B eB,secEq B B eB)
-              , (i = 0) -> (A,w.1,invEq A B w,retEq A B w,secEq A B w) ]
 -  <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.1,invEq A B e,retEq A B e,secEq A B e)
-            , (i = 1) -> (B,f.1,invEq B B f,retEq B B f,secEq B B f)
-            , (j = 1) -> (p@i,g.1,invEq Ai B g,retEq Ai B g,secEq Ai B g) ]
 -           [ (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 (trans A B (transEquivToId A B w)) =
 -  : Id (A -> B) w.1 (transEquiv A B (transEquivToId A B w)).1 =
-- <i> \ (a:A) -> 
--   let b : B = w.1 a
-    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]
 -       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)
 -
--
--
--
++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)