simplified transIdFun

diff --git a/examples/testEquiv.ctt b/examples/testEquiv.ctt
index 70b188f988e531a579c9369968257c14c856b92e..496f6f869e471abb1e68a15ffc8ea5cfacf827c8 100644 (file)
--- a/examples/testEquiv.ctt
+++ b/examples/testEquiv.ctt
@@ -95,17 +95,14 @@ eqToEq (A B : U) (p : Id U A B)
            , (j = 1) -> (p@i,g.1,invEq Ai B g,retEq Ai B g,secEq Ai B g) ]\r
 \r
 transIdFun (A B : U) (w : equiv A B)\r
-  : Id (A -> B) (trans A B (transEquivToId A B w)) w.1 =\r
-  <i> \(a : A) -> let b : B = w.1 a\r
-                  in addf (f (f (f b))) b (addf (f (f b)) b (addf (f b) b (trf b))) @ i\r
-  where f (b : B) : B = comp (<_> B) b []\r
-        trf (b : B) : Id B (f b) b =\r
-          <i> fill (<_> B) b [] @ -i\r
-        addf (b b' : B) : Id B b b' -> Id B (f b) b' =\r
-          compId B (f b) b b' (trf b)\r
+  : Id (A -> B) w.1 (trans A B (transEquivToId A B w)) =\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
 \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
-      (transIdFun A B w)\r
+      (<i>transIdFun A B w@-i)\r
+\r
 \r