comments

diff --git a/examples/univalence.ctt b/examples/univalence.ctt
index b015cefcef20210ffb7d55e0b8782efc27cd5023..ec4675a033b437be26ebe6f31d2513ce4b386d49 100644 (file)
--- a/examples/univalence.ctt
+++ b/examples/univalence.ctt
@@ -211,16 +211,17 @@ uabeta (A B : U) (e : equiv A B) : Path (A -> B) (trans A B (ua A B e)) e.1 =
 
 -- uabeta implies that equiv A B is a retract of Path U A B
 
--- We don't have to use transEquivDirect:
+-- We don't have to use transEquivDirect as below:
 -- uaret (A B : U) : retract (equiv A B) (Path U A B) (ua A B) (transEquivDirect A B) =
 --   \(e : equiv A B) ->
 --     equivLemma A B (transEquivDirect A B (ua A B e)) e (uabeta A B e)
 
+-- Instead we prove uabeta for transEquiv:
+uabetaTransEquiv (A B : U) (e : equiv A B) : Path (A -> B) (transEquiv A B (ua A B e)).1 e.1 =
+  <i> \(a : A) -> (uabeta A B e @ i) (fill (<_> A) a [] @ -i)
+
 uaret (A B : U) : retract (equiv A B) (Path U A B) (ua A B) (transEquiv A B) =
-  \(e : equiv A B) ->
-  let rem (a : A) : Path B ((transEquiv A B (ua A B e)).1 a) (e.1 a) =
-        <i> (uabeta A B e @ i) (fill (<_> A) a [] @ -i)
-  in equivLemma A B (transEquiv A B (ua A B e)) e (<i> \(a : A) -> rem a @ i)
+  \(e : equiv A B) -> equivLemma A B (transEquiv A B (ua A B e)) e (uabetaTransEquiv A B e)
 
 -- So  (B:U) x equiv A B    is a retract of    (B:U) x Path U A B
 f1 (A : U) (p : (B : U) * equiv A B) : ((B : U) * Path U A B) = (p.1,ua A p.1 p.2)