proof relating function part of transEquiv to transEquivDirect

diff --git a/examples/equiv.ctt b/examples/equiv.ctt
index 60fd32c19fdd75b232f78fc9eea8ea9eaab4a9dd..dc2f405e035d2fdd0ed1acfc8dfe9a3fa4c3b5b5 100644 (file)
--- a/examples/equiv.ctt
+++ b/examples/equiv.ctt
@@ -108,7 +108,7 @@ secEq (A B:U) (w:equiv A B) (x:A) : Path A (invEq A B w (w.1 x)) x =
 
 transEquivDirect (A B:U) (p:Path U A B) : equiv A B = (f,p)
  where
-  f (x:A) : B = comp p x []
+  f (x:A) : B = trans A B p x
   g (y:B) : A = comp (<i>p@-i) y []
   lem1 (x:A) : PathP p x (f x) = <i>comp (<j>p@(i/\j)) x [(i=0) -> <j>x]
   lem2 (y:B) : PathP p (g y) y = <i>comp (<j>p@(i\/-j)) y [(i=1) -> <j>y]
@@ -131,8 +131,15 @@ lemSinglContr (A:U) (a:A) : isContr ((x:A) * Path A a x) =
 
 idEquiv (A:U) : equiv A A = (\ (x:A) -> x, lemSinglContr A)
 
-transEquiv (A X:U) (p:Path U A X) : equiv A X =
- subst U (equiv A) A X p (idEquiv A)
+transEquiv (A B : U) (p : Path U A B) : equiv A B =
+ subst U (equiv A) A B p (idEquiv A)
+
+compf (A B C : U) (f : B -> C) (g : A -> B) : A -> C =
+  \(a : A) -> f (g a)
+
+transEquivEq (A B : U) (p : Path U A B) :
+  Path (A -> B) (transEquiv A B p).1 (compf A A B (trans A B p) (trans A A (<_> A))) =
+  <_> (transEquiv A B p).1
 
 transDelta (A:U) : equiv A A = transEquiv A A (<i>A)