From 7a6d2ea8ff1d1ad168a837e4c6ee87fb9ae234d3 Mon Sep 17 00:00:00 2001
From: =?utf8?q?Anders=20M=C3=B6rtberg?= <andersmortberg@gmail.com>
Date: Mon, 20 Nov 2017 18:42:11 -0500
Subject: [PATCH] improve uaret

---
 examples/equiv.ctt      |  5 +++--
 examples/univalence.ctt | 27 ++++++++++++---------------
 2 files changed, 15 insertions(+), 17 deletions(-)

diff --git a/examples/equiv.ctt b/examples/equiv.ctt
index 81d063f..60fd32c 100644
--- a/examples/equiv.ctt
+++ b/examples/equiv.ctt
@@ -84,9 +84,10 @@ propIsEquivDirect' (A B : U) (f : A -> B) : prop (isEquiv A B f) =
                                                         , (j = 1) -> <k> x ] @ k) ]
           in <j> (sq1 @ i @ j,sq2 @ i @ j))
 
+-- Using propIsEquivDirect here makes this a lot faster to use later
 equivLemma (A B : U)
   : (v w : equiv A B) -> Path (A -> B) v.1 w.1 -> Path (equiv A B) v w
-  = lemSig (A -> B) (isEquiv A B) (propIsEquiv A B)
+  = lemSig (A -> B) (isEquiv A B) (propIsEquivDirect A B)
 
 idIsEquiv (A : U) : isEquiv A A (idfun A) =
   \(a : A) -> ((a, refl A a)
@@ -131,7 +132,7 @@ 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 =
- substTrans U (equiv A) A X p (idEquiv A)
+ subst U (equiv A) A X p (idEquiv A)
 
 transDelta (A:U) : equiv A A = transEquiv A A (<i>A)
 
diff --git a/examples/univalence.ctt b/examples/univalence.ctt
index 70bf026..a8f0e0e 100644
--- a/examples/univalence.ctt
+++ b/examples/univalence.ctt
@@ -207,31 +207,28 @@ ua (A B : U) (e : equiv A B) : Path U A B =
 -- have been the identity function (i.e. if the computation rule for J
 -- would be definitional) this proof would be trivial.
 uabeta (A B : U) (e : equiv A B) : Path (A -> B) (trans A B (ua A B e)) e.1 =
-  <i> \(a : A) ->
-      let b : B = trans B B (<_> B) (e.1 a)
-          rem1 : Path B b (e.1 a) = <i> fill (<_> B) (e.1 a) [] @ -i
-          rem2 : Path B (trans B B (<_> B) b) b = <i> fill (<_> B) b [] @ -i
-          goal : Path B (trans B B (<_> B) b) (e.1 a) =
-            compPath B (trans B B (<_> B) b) b (e.1 a) rem2 rem1
-      in goal @ i
+  <i> \(a : A) -> fill (<_> B) (fill (<_> B) (e.1 a) [] @ -i) [] @ -i
 
 -- uabeta implies that equiv A B is a retract of Path U A B
-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)
 
+-- We don't have to use transEquivDirect:
+-- 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)
 
--- So  (B:U) x equiv A B    is a retract of    (B:U) x Path U A B
-opaque uaret
+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> fill (<_> B) (fill (<_> B) (e.1 (fill (<_> A) a [] @ -i)) [] @ -i) [] @ -i
+  in equivLemma A B (transEquiv A B (ua A B e)) e (<i> \(a : A) -> rem a @ i)
 
+-- 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)
-f2 (A : U) (p : (B : U) * Path U A B) : ((B : U) * equiv A B) = (p.1,transEquivDirect A p.1 p.2)
+f2 (A : U) (p : (B : U) * Path U A B) : ((B : U) * equiv A B) = (p.1,transEquiv A p.1 p.2)
 
 uaretsig (A : U) : retract ((B : U) * equiv A B) ((B : U) * Path U A B) (f1 A) (f2 A) =
   \(p : (B : U) * equiv A B) -> <i> (p.1,uaret A p.1 p.2 @ i)
 
-transparent uaret
-
 -- But   (B : U) x Path U A B   is contractible
 isContrPath (A : U) : isContr ((B : U) * Path U A B) =
   let ctr : (B : U) * Path U A B = (A,<_> A)
-- 
2.34.1