From: Anders Mörtberg <andersmortberg@gmail.com>
Date: Mon, 4 Jan 2016 18:18:40 +0000 (+0100)
Subject: Refactoring and move old code on equivalences to experiments folder
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=26b70046ce7e45197f14ead82daae7e0354e9945;p=cubicaltt.git

Refactoring and move old code on equivalences to experiments folder
---

diff --git a/examples/equiv.ctt b/examples/equiv.ctt
index 52155a9..fc15018 100644
--- a/examples/equiv.ctt
+++ b/examples/equiv.ctt
@@ -1,262 +1,180 @@
-module equiv where
-
-import prelude
-
-fiber (A B : U) (f : A -> B) (y : B) : U =
-  (x : A) * Id B (f x) y
-
-isEquiv (A B : U) (f : A -> B) : U =
-    (s : (y : B) -> fiber A B f y)
-  * ((y : B) (w : fiber A B f y) -> Id (fiber A B f y) (s y) w)
-
-equiv (A B : U) : U = (f : A -> B) * isEquiv A B f
-
-propIsEquiv (A B : U) (f : A -> B)
-  : prop (isEquiv A B f) = lemProp (isEquiv A B f) lem
-  where
-    isEqf : U = isEquiv A B f
-    fibf : (y : B) -> U = fiber A B f
-    center : U = (y : B) -> fibf y
-    isCenter (s : center) : U = (y : B) (w : fibf y) -> Id (fibf y) (s y) w
-    lem (fe : isEqf) : prop isEqf = propSig center isCenter pc pisc
-      where
-        fibprop (y : B) (u v : fibf y) : Id (fibf y) u v =
-          compId (fibf y) u (fe.1 y) v (<i> fe.2 y u @ -i) (fe.2 y v)
-        pc : prop center = propPi B fibf fibprop
-        pisc (s : center) (g h : isCenter s) : Id (isCenter s) g h =
-          <i> \ (y : B) (w : fibf y) ->
-                 propSet (fibf y) (fibprop y) (s y) w (g y w) (h y w) @ i
-
-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)
-
-
--- The identity function is an equivalence
-idCenter (A : U) (y : A) : fiber A A (idfun A) y = (y, refl A y)
-
--- TODO: redifine fiber so this gets nicer?
-idIsCenter (A : U) (y : A) (w : fiber A A (idfun A) y)
-  : Id (fiber A A (idfun A) y) (idCenter A y) w =
-  <i> (w.2 @ -i, <j> w.2 @ j \/ -i)
-
-idIsEquiv (A : U) : isEquiv A A (idfun A) = (idCenter A,idIsCenter A)
-
-idEquiv (A : U) : equiv A A = (idfun A, idIsEquiv A)
-
--- Transport is an equivalence
--- NB: The proof is taken from the output of a comp U
-trans (A B : U) (p : Id U A B) (a : A) : B = transport p a
-
-transCenter (A B : U) (p : Id U A B) (y : B) : fiber A B (trans A B p) y =
-  (comp (<i0> p @ -i0) y []
-  ,<i0> comp p (comp (<i0> p @ -i0) y [])
-          [ (i0 = 0) -> <i1> comp (<i2> p @ (i1 /\ i2)) (comp (<i0> p @ -i0) y [])
-                               [ (i1 = 0) -> <i2> comp (<i0> p @ -i0) y [] ]
-          , (i0 = 1) -> <i1> comp (<i2> p @ (i1 \/ -i2)) y [ (i1 = 1) -> <i2> y ] ])
-
-transIsCenter (A B : U) (p : Id U A B) (y : B) (w : fiber A B (trans A B p) y)
-  : Id (fiber A B (trans A B p) y) (transCenter A B p y) w
-  = <i0>
-    ( comp (<i1> p @ -i1) (w.2 @ -i0)
-           [ (i0 = 0) -> <i1> comp (<i2> p @ (-i1 \/ -i2)) y [ (i1 = 0) -> <i2> y ]
-           , (i0 = 1) -> <i1> comp (<i2> p @ (-i1 /\ i2)) (w.1) [ (i1 = 1) -> <i2> w.1 ] ]
-    , <i1> comp (<i2> p @ i2)
-             (comp (<i2> p @ -i2) (w.2 @ (-i0 \/ i1))
-               [ (i0 = 0) -> <i2> comp (<i3> p @ (-i2 \/ -i3)) y [ (i2 = 0) -> <i3> y ]
-               , (i0 = 1)(i1 = 0) ->
-                    <i2> comp (<i3> p @ (-i2 /\ i3)) (w.1)
-                           [ (i2 = 1) -> <i3> w.1 ]
-               , (i1 = 1) -> <i2> comp (<i3> p @ (-i2 \/ -i3)) y [ (i2 = 0) -> <i3> y ] ])
-             [ (i0 = 0) -> <i2> comp (<i3> p @ (i2 /\ i3))
-                                  (comp (<i0> p @ -i0) y [  ])
-                                  [ (i1 = 0) ->
-                                      <i3> comp (<i4> p @ (i2 /\ i3 /\ i4))
-                                             (comp (<i0> p @ -i0) y [  ])
-                                             [ (i2 = 0) -> <i4> comp (<i0> p @ -i0) y [  ]
-                                             , (i3 = 0) -> <i4> comp (<i0> p @ -i0) y [  ] ]
-                                  , (i1 = 1) ->
-                                      <i3> comp (<i4> p @ ((i2 /\ i3) \/ -i4)) y
-                                             [ (i2 = 1)(i3 = 1) -> <i4> y ]
-                                  , (i2 = 0) -> <i3> comp (<i0> p @ -i0) y [  ] ]
-             , (i0 = 1) ->
-                  <i2> comp (<i3> p @ (i2 \/ -i3)) (w.2 @ i1)
-                         [ (i1 = 0) ->
-                              <i3> comp (<i4> p @ ((i2 /\ i4) \/ (-i3 /\ i4))) (w.1)
-                                     [ (i2 = 0)(i3 = 1) -> <i4> w.1 ]
-                         , (i1 = 1) ->
-                              <i3> comp (<i4> p @ (i2 \/ -i3 \/ -i4)) y
-                                     [ (i2 = 1) -> <i4> y, (i3 = 0) -> <i4> y ]
-                         , (i2 = 1) -> <i3> w.2 @ i1 ]
-             , (i1 = 0) ->
-                 <i2> comp (<i3> p @ (i2 /\ i3))
-                        (comp (<i1> p @ -i1) (w.2 @ -i0)
-                           [ (i0 = 0) ->
-                               <i1> comp (<i2> p @ (-i1 \/ -i2)) y [ (i1 = 0) -> <i2> y ]
-                           , (i0 = 1) ->
-                                <i1> comp (<i2> p @ (-i1 /\ i2)) (w.1)
-                                       [ (i1 = 1) -> <i2> w.1 ]
-                           ])
-                        [ (i2 = 0) ->
-                             <i3> comp (<i1> p @ -i1) (w.2 @ -i0)
-                                    [ (i0 = 0) ->
-                                         <i1> comp (<i2> p @ (-i1 \/ -i2)) y
-                                                [ (i1 = 0) -> <i2> y ]
-                                    , (i0 = 1) ->
-                                        <i1> comp (<i2> p @ (-i1 /\ i2)) (w.1)
-                                               [ (i1 = 1) -> <i2> w.1 ]
-                                    ]
-                        ]
-             , (i1 = 1) -> <i2> comp (<i3> p @ (i2 \/ -i3)) y [ (i2 = 1) -> <i3> y ] ]
-    )
-
-transIsEquiv (A B : U) (p : Id U A B) : isEquiv A B (trans A B p) =
-  (transCenter A B p,transIsCenter A B p)
-
-transEquiv (A B : U) (p : Id U A B) : equiv A B =
-  (trans A B p,transIsEquiv A B p)
-
-transDelta (A : U) : equiv A A = transEquiv A A (<_> A)
-
-
-invEquiv (A B : U) (f : A -> B) (is : isEquiv A B f) (y : B) : A = (is.1 y).1
-
-invEq (A B : U) (f : equiv A B) : B -> A = invEquiv A B f.1 f.2
-
-
-retEquiv (A B : U) (f : A -> B) (is : isEquiv A B f) (y : B) :
-  Id B (f (invEquiv A B f is y)) y = (is.1 y).2
-
-retEq (A B : U) (f:equiv A B) : (y:B) -> Id B (f.1 (invEq A B f y)) y =
- retEquiv A B f.1 f.2
-
-secEquiv (A B : U) (f : A -> B) (is : isEquiv A B f) (x : A) :
-  Id A (invEquiv A B f is (f x)) x = <i> (is.2 (f x) (x, <_> f x) @ i).1
-
-secEq (A B : U) (f: equiv A B) : (x:A) -> Id A (invEq A B f (f.1 x)) x =
- secEquiv A B f.1 f.2
-
-
--- Alternative definition:
-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
-
-
-
-
--- Another alternative definitions:
-
--- isContr (A : U) : U = and (prop A) A
-
--- fiber (A B:U) (f:A->B) (b:B) : U = (x:A) * Id B b (f x)
-
--- lemIdFib (A:U) (a:A) : prop (fiber A A (\ (x:A) -> x) a) = rem
---  where F : U = fiber A A (\ (x:A) -> x) a
---        rem (u v:F) : Id F u v = <i>(rem1 @ i,rem2 @ i)
---          where x : A = u.1
---                p : Id A a x = u.2
---                y : A = v.1
---                q : Id A a y = v.2
---                rem1 : Id A x y = <i>comp A a [(i=0) -> p,(i=1) -> q]
---                rem2 : IdP (<i>Id A a (rem1@i)) p q = <i j>comp A a [(i=0) -> <l>p@(j/\l),(i=1) -> <l>q@(j/\l)]
-
--- lemPropAnd (A B :U) (pA: prop A) (pB: A -> prop B) : prop (and A B) = 
---  \ (u v:and A B) -> <i>((pA u.1 v.1)@i, (pB u.1 u.2 v.2)@i)
-
--- isContrProp (A:U) : prop (isContr A) = 
---  lemPropAnd (prop A) A (propIsProp A) (\ (h:prop A) -> h)
-
--- 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) -> (lemIdFib A a,(a,refl A a))
-
--- propIsEquiv (A B : U) (f : A -> B) : prop (isEquiv A B f)
---  = propPi B (\ (y:B) -> isContr (fiber A B f y)) (\ (y:B) -> isContrProp (fiber A B f y))
-
--- isEquivEq (A B : U) (f : A -> B) (is:isEquiv A B f) : Id U A B = 
---  isoId A B f g (\ (y:B) -> <i>(s y)@-i) t
---  where
---    rem1 (y:B) : prop (fiber A B f y) =  (is y).1
---    rem2 (y:B) : fiber A B f y        =  (is y).2
---    g (y:B) : A = (rem2 y).1
---    s (y:B) : Id B y (f (g y)) = (rem2 y).2
---    rem3 (x:A) : Id B (f x) (f (g (f x))) = s (f x)
---    rem4 (x:A) : Id (fiber A B f (f x)) (g (f x),rem3 x) (x,refl B (f x)) = 
---      rem1 (f x) (g (f x),rem3 x) (x,refl B (f x))
---    t (x:A) : Id A (g (f x)) x = <i> ((rem4 x)@i).1
-    
--- Equiv (A B : U) : U = (f : A -> B) * isEquiv A B f
-
--- lemIdEquiv (A B:U) (f g : Equiv A B) (h:Id (A->B) f.1 g.1) : Id (Equiv A B) f g
---  = <i>(h@i,(lemPropF (A->B) (isEquiv A B) (propIsEquiv A B) f.1 g.1 h f.2 g.2)@i)
-
--- -- a general lemma about equivalence and fibrations
-
--- Sigma (A:U) (F:A->U) : U = (x:A) * F x
-
--- lemEquivFib (A:U) (F G :A -> U) (f:(x:A) -> F x -> G x)
---    (h : isEquiv (Sigma A F) (Sigma A G) (\ (xp : Sigma A F) -> (xp.1,f xp.1 xp.2))) (x:A) (v:G x) : 
---     isContr (fiber (F x) (G x) (f x) v) = (rem7,psi (rem1.2))
---  where
---    AF : U = Sigma A F
---    AG : U = Sigma A G
---    g (xp : AF) : AG = (xp.1,f xp.1 xp.2)
---    rem1 : isContr (fiber AF AG g (x,v)) = h (x,v)
---    phi (z:fiber (F x) (G x) (f x) v) : fiber AF AG g (x,v) = ((x,z.1),<i>(x,(z.2)@ i))
---    psi (z:fiber AF AG g (x,v)) : fiber (F x) (G x) (f x) v = transport (<i> (u : F (p@-i)) * IdP (<j>G (p@-i /\ j)) v (f (p@-i) u)) (w,q)
---       where yu : AF = z.1
---             y : A = yu.1
---             w : F y = yu.2
---             p : Id A x y = <i>(z.2 @ i).1
---             q : IdP (<j>G (p@j)) v (f y w) = <i>((z.2) @ i).2
---    rem7 (z0 z1 : fiber (F x) (G x) (f x) v) : Id (fiber (F x) (G x) (f x) v) z0 z1 = <i>psi ((rem1.1 (phi z0) (phi z1))@i)
-
+-- This file contains the definition of equivalences and various
+-- results on these, including the "graduate lemma".
+module equiv 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)
diff --git a/examples/testEquiv.ctt b/examples/testEquiv.ctt
deleted file mode 100644
index 4059918..0000000
--- a/examples/testEquiv.ctt
+++ /dev/null
@@ -1,178 +0,0 @@
-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)
diff --git a/examples/testUniv.ctt b/examples/testUniv.ctt
index ecd0299..8662cda 100644
--- a/examples/testUniv.ctt
+++ b/examples/testUniv.ctt
@@ -1,7 +1,7 @@
 module testUniv where
 
 import testContr
-import testEquiv
+import equiv
 
 swap : bool -> bool = split
  true -> false
diff --git a/experiments/equiv.ctt b/experiments/equiv.ctt
new file mode 100644
index 0000000..7dc743b
--- /dev/null
+++ b/experiments/equiv.ctt
@@ -0,0 +1,264 @@
+-- This file contains the old definition of equivalence and various
+-- results on these
+module equiv where
+
+import prelude
+
+fiber (A B : U) (f : A -> B) (y : B) : U =
+  (x : A) * Id B (f x) y
+
+isEquiv (A B : U) (f : A -> B) : U =
+    (s : (y : B) -> fiber A B f y)
+  * ((y : B) (w : fiber A B f y) -> Id (fiber A B f y) (s y) w)
+
+equiv (A B : U) : U = (f : A -> B) * isEquiv A B f
+
+propIsEquiv (A B : U) (f : A -> B)
+  : prop (isEquiv A B f) = lemProp (isEquiv A B f) lem
+  where
+    isEqf : U = isEquiv A B f
+    fibf : (y : B) -> U = fiber A B f
+    center : U = (y : B) -> fibf y
+    isCenter (s : center) : U = (y : B) (w : fibf y) -> Id (fibf y) (s y) w
+    lem (fe : isEqf) : prop isEqf = propSig center isCenter pc pisc
+      where
+        fibprop (y : B) (u v : fibf y) : Id (fibf y) u v =
+          compId (fibf y) u (fe.1 y) v (<i> fe.2 y u @ -i) (fe.2 y v)
+        pc : prop center = propPi B fibf fibprop
+        pisc (s : center) (g h : isCenter s) : Id (isCenter s) g h =
+          <i> \ (y : B) (w : fibf y) ->
+                 propSet (fibf y) (fibprop y) (s y) w (g y w) (h y w) @ i
+
+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)
+
+
+-- The identity function is an equivalence
+idCenter (A : U) (y : A) : fiber A A (idfun A) y = (y, refl A y)
+
+-- TODO: redifine fiber so this gets nicer?
+idIsCenter (A : U) (y : A) (w : fiber A A (idfun A) y)
+  : Id (fiber A A (idfun A) y) (idCenter A y) w =
+  <i> (w.2 @ -i, <j> w.2 @ j \/ -i)
+
+idIsEquiv (A : U) : isEquiv A A (idfun A) = (idCenter A,idIsCenter A)
+
+idEquiv (A : U) : equiv A A = (idfun A, idIsEquiv A)
+
+-- Transport is an equivalence
+-- NB: The proof is taken from the output of a comp U
+trans (A B : U) (p : Id U A B) (a : A) : B = transport p a
+
+transCenter (A B : U) (p : Id U A B) (y : B) : fiber A B (trans A B p) y =
+  (comp (<i0> p @ -i0) y []
+  ,<i0> comp p (comp (<i0> p @ -i0) y [])
+          [ (i0 = 0) -> <i1> comp (<i2> p @ (i1 /\ i2)) (comp (<i0> p @ -i0) y [])
+                               [ (i1 = 0) -> <i2> comp (<i0> p @ -i0) y [] ]
+          , (i0 = 1) -> <i1> comp (<i2> p @ (i1 \/ -i2)) y [ (i1 = 1) -> <i2> y ] ])
+
+transIsCenter (A B : U) (p : Id U A B) (y : B) (w : fiber A B (trans A B p) y)
+  : Id (fiber A B (trans A B p) y) (transCenter A B p y) w
+  = <i0>
+    ( comp (<i1> p @ -i1) (w.2 @ -i0)
+           [ (i0 = 0) -> <i1> comp (<i2> p @ (-i1 \/ -i2)) y [ (i1 = 0) -> <i2> y ]
+           , (i0 = 1) -> <i1> comp (<i2> p @ (-i1 /\ i2)) (w.1) [ (i1 = 1) -> <i2> w.1 ] ]
+    , <i1> comp (<i2> p @ i2)
+             (comp (<i2> p @ -i2) (w.2 @ (-i0 \/ i1))
+               [ (i0 = 0) -> <i2> comp (<i3> p @ (-i2 \/ -i3)) y [ (i2 = 0) -> <i3> y ]
+               , (i0 = 1)(i1 = 0) ->
+                    <i2> comp (<i3> p @ (-i2 /\ i3)) (w.1)
+                           [ (i2 = 1) -> <i3> w.1 ]
+               , (i1 = 1) -> <i2> comp (<i3> p @ (-i2 \/ -i3)) y [ (i2 = 0) -> <i3> y ] ])
+             [ (i0 = 0) -> <i2> comp (<i3> p @ (i2 /\ i3))
+                                  (comp (<i0> p @ -i0) y [  ])
+                                  [ (i1 = 0) ->
+                                      <i3> comp (<i4> p @ (i2 /\ i3 /\ i4))
+                                             (comp (<i0> p @ -i0) y [  ])
+                                             [ (i2 = 0) -> <i4> comp (<i0> p @ -i0) y [  ]
+                                             , (i3 = 0) -> <i4> comp (<i0> p @ -i0) y [  ] ]
+                                  , (i1 = 1) ->
+                                      <i3> comp (<i4> p @ ((i2 /\ i3) \/ -i4)) y
+                                             [ (i2 = 1)(i3 = 1) -> <i4> y ]
+                                  , (i2 = 0) -> <i3> comp (<i0> p @ -i0) y [  ] ]
+             , (i0 = 1) ->
+                  <i2> comp (<i3> p @ (i2 \/ -i3)) (w.2 @ i1)
+                         [ (i1 = 0) ->
+                              <i3> comp (<i4> p @ ((i2 /\ i4) \/ (-i3 /\ i4))) (w.1)
+                                     [ (i2 = 0)(i3 = 1) -> <i4> w.1 ]
+                         , (i1 = 1) ->
+                              <i3> comp (<i4> p @ (i2 \/ -i3 \/ -i4)) y
+                                     [ (i2 = 1) -> <i4> y, (i3 = 0) -> <i4> y ]
+                         , (i2 = 1) -> <i3> w.2 @ i1 ]
+             , (i1 = 0) ->
+                 <i2> comp (<i3> p @ (i2 /\ i3))
+                        (comp (<i1> p @ -i1) (w.2 @ -i0)
+                           [ (i0 = 0) ->
+                               <i1> comp (<i2> p @ (-i1 \/ -i2)) y [ (i1 = 0) -> <i2> y ]
+                           , (i0 = 1) ->
+                                <i1> comp (<i2> p @ (-i1 /\ i2)) (w.1)
+                                       [ (i1 = 1) -> <i2> w.1 ]
+                           ])
+                        [ (i2 = 0) ->
+                             <i3> comp (<i1> p @ -i1) (w.2 @ -i0)
+                                    [ (i0 = 0) ->
+                                         <i1> comp (<i2> p @ (-i1 \/ -i2)) y
+                                                [ (i1 = 0) -> <i2> y ]
+                                    , (i0 = 1) ->
+                                        <i1> comp (<i2> p @ (-i1 /\ i2)) (w.1)
+                                               [ (i1 = 1) -> <i2> w.1 ]
+                                    ]
+                        ]
+             , (i1 = 1) -> <i2> comp (<i3> p @ (i2 \/ -i3)) y [ (i2 = 1) -> <i3> y ] ]
+    )
+
+transIsEquiv (A B : U) (p : Id U A B) : isEquiv A B (trans A B p) =
+  (transCenter A B p,transIsCenter A B p)
+
+transEquiv (A B : U) (p : Id U A B) : equiv A B =
+  (trans A B p,transIsEquiv A B p)
+
+transDelta (A : U) : equiv A A = transEquiv A A (<_> A)
+
+
+invEquiv (A B : U) (f : A -> B) (is : isEquiv A B f) (y : B) : A = (is.1 y).1
+
+invEq (A B : U) (f : equiv A B) : B -> A = invEquiv A B f.1 f.2
+
+
+retEquiv (A B : U) (f : A -> B) (is : isEquiv A B f) (y : B) :
+  Id B (f (invEquiv A B f is y)) y = (is.1 y).2
+
+retEq (A B : U) (f:equiv A B) : (y:B) -> Id B (f.1 (invEq A B f y)) y =
+ retEquiv A B f.1 f.2
+
+secEquiv (A B : U) (f : A -> B) (is : isEquiv A B f) (x : A) :
+  Id A (invEquiv A B f is (f x)) x = <i> (is.2 (f x) (x, <_> f x) @ i).1
+
+secEq (A B : U) (f: equiv A B) : (x:A) -> Id A (invEq A B f (f.1 x)) x =
+ secEquiv A B f.1 f.2
+
+
+-- Alternative definition:
+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
+
+
+
+
+-- Another alternative definitions:
+
+-- isContr (A : U) : U = and (prop A) A
+
+-- fiber (A B:U) (f:A->B) (b:B) : U = (x:A) * Id B b (f x)
+
+-- lemIdFib (A:U) (a:A) : prop (fiber A A (\ (x:A) -> x) a) = rem
+--  where F : U = fiber A A (\ (x:A) -> x) a
+--        rem (u v:F) : Id F u v = <i>(rem1 @ i,rem2 @ i)
+--          where x : A = u.1
+--                p : Id A a x = u.2
+--                y : A = v.1
+--                q : Id A a y = v.2
+--                rem1 : Id A x y = <i>comp A a [(i=0) -> p,(i=1) -> q]
+--                rem2 : IdP (<i>Id A a (rem1@i)) p q = <i j>comp A a [(i=0) -> <l>p@(j/\l),(i=1) -> <l>q@(j/\l)]
+
+-- lemPropAnd (A B :U) (pA: prop A) (pB: A -> prop B) : prop (and A B) = 
+--  \ (u v:and A B) -> <i>((pA u.1 v.1)@i, (pB u.1 u.2 v.2)@i)
+
+-- isContrProp (A:U) : prop (isContr A) = 
+--  lemPropAnd (prop A) A (propIsProp A) (\ (h:prop A) -> h)
+
+-- 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) -> (lemIdFib A a,(a,refl A a))
+
+-- propIsEquiv (A B : U) (f : A -> B) : prop (isEquiv A B f)
+--  = propPi B (\ (y:B) -> isContr (fiber A B f y)) (\ (y:B) -> isContrProp (fiber A B f y))
+
+-- isEquivEq (A B : U) (f : A -> B) (is:isEquiv A B f) : Id U A B = 
+--  isoId A B f g (\ (y:B) -> <i>(s y)@-i) t
+--  where
+--    rem1 (y:B) : prop (fiber A B f y) =  (is y).1
+--    rem2 (y:B) : fiber A B f y        =  (is y).2
+--    g (y:B) : A = (rem2 y).1
+--    s (y:B) : Id B y (f (g y)) = (rem2 y).2
+--    rem3 (x:A) : Id B (f x) (f (g (f x))) = s (f x)
+--    rem4 (x:A) : Id (fiber A B f (f x)) (g (f x),rem3 x) (x,refl B (f x)) = 
+--      rem1 (f x) (g (f x),rem3 x) (x,refl B (f x))
+--    t (x:A) : Id A (g (f x)) x = <i> ((rem4 x)@i).1
+    
+-- Equiv (A B : U) : U = (f : A -> B) * isEquiv A B f
+
+-- lemIdEquiv (A B:U) (f g : Equiv A B) (h:Id (A->B) f.1 g.1) : Id (Equiv A B) f g
+--  = <i>(h@i,(lemPropF (A->B) (isEquiv A B) (propIsEquiv A B) f.1 g.1 h f.2 g.2)@i)
+
+-- -- a general lemma about equivalence and fibrations
+
+-- Sigma (A:U) (F:A->U) : U = (x:A) * F x
+
+-- lemEquivFib (A:U) (F G :A -> U) (f:(x:A) -> F x -> G x)
+--    (h : isEquiv (Sigma A F) (Sigma A G) (\ (xp : Sigma A F) -> (xp.1,f xp.1 xp.2))) (x:A) (v:G x) : 
+--     isContr (fiber (F x) (G x) (f x) v) = (rem7,psi (rem1.2))
+--  where
+--    AF : U = Sigma A F
+--    AG : U = Sigma A G
+--    g (xp : AF) : AG = (xp.1,f xp.1 xp.2)
+--    rem1 : isContr (fiber AF AG g (x,v)) = h (x,v)
+--    phi (z:fiber (F x) (G x) (f x) v) : fiber AF AG g (x,v) = ((x,z.1),<i>(x,(z.2)@ i))
+--    psi (z:fiber AF AG g (x,v)) : fiber (F x) (G x) (f x) v = transport (<i> (u : F (p@-i)) * IdP (<j>G (p@-i /\ j)) v (f (p@-i) u)) (w,q)
+--       where yu : AF = z.1
+--             y : A = yu.1
+--             w : F y = yu.2
+--             p : Id A x y = <i>(z.2 @ i).1
+--             q : IdP (<j>G (p@j)) v (f y w) = <i>((z.2) @ i).2
+--    rem7 (z0 z1 : fiber (F x) (G x) (f x) v) : Id (fiber (F x) (G x) (f x) v) z0 z1 = <i>psi ((rem1.1 (phi z0) (phi z1))@i)
+
diff --git a/examples/gradLemma.ctt b/experiments/gradLemma.ctt
similarity index 98%
rename from examples/gradLemma.ctt
rename to experiments/gradLemma.ctt
index 41ab643..fa01e27 100644
--- a/examples/gradLemma.ctt
+++ b/experiments/gradLemma.ctt
@@ -1,3 +1,5 @@
+-- This file contains a proof of the graduate lemma using the old
+-- version of equivalence
 module gradLemma where
 
 import equiv
diff --git a/examples/univalence.ctt b/experiments/univalence.ctt
similarity index 94%
rename from examples/univalence.ctt
rename to experiments/univalence.ctt
index ac236fa..58d5ae5 100644
--- a/examples/univalence.ctt
+++ b/experiments/univalence.ctt
@@ -1,10 +1,11 @@
+-- The old version of univalence using the old definition of equivalences
 module univalence where
 
 import gradLemma
 
 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)