From bf8253f482917e390fe8b44ceaf308405afeefc6 Mon Sep 17 00:00:00 2001
From: Carlo Angiuli <carlo@carloangiuli.com>
Date: Mon, 9 Apr 2018 15:11:27 -0400
Subject: [PATCH] Clean up isoToEquiv proof with Anders.

---
 examples/equiv.ctt | 35 ++++++++++++++---------------------
 1 file changed, 14 insertions(+), 21 deletions(-)

diff --git a/examples/equiv.ctt b/examples/equiv.ctt
index dc2f405..a8e4ba1 100644
--- a/examples/equiv.ctt
+++ b/examples/equiv.ctt
@@ -185,36 +185,29 @@ lemIso (A B : U) (f : A -> B) (g : B -> A)
     rem0 : Path A (g y) x0 =
       <i> comp (<k> A) (g (p0 @ i)) [ (i = 1) -> t x0, (i = 0) -> <k> g y ]
 
+    rem0fill : Square A (g y) (g (f x0)) (g y) x0
+                        (<i> g (p0 @ i)) rem0 (<i> g y) (t x0)  =
+      <i> fill (<k> A) (g (p0 @ i)) [ (i = 1) -> t x0, (i = 0) -> <k> g y ]
+
     rem1 : Path A (g y) x1 =
       <i> comp (<k> A) (g (p1 @ i)) [ (i = 1) -> t x1, (i = 0) -> <k> g y ]
 
+    rem1fill : Square A (g y) (g (f x1)) (g y) x1
+                        (<i> g (p1 @ i)) rem1 (<i> g y) (t x1) =
+      <i> fill (<k> A) (g (p1 @ i)) [ (i = 1) -> t x1, (i = 0) -> <k> g y ]
+
     p : Path A x0 x1 =
-     <i> comp (<k> 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 (<k> A) (g (p0 @ i)) [ (i = 1) -> <k> t x0 @ j /\ k
-                                      , (i = 0) -> <k> g y
-                                      , (j = 0) -> <k> 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 (<k> A) (g (p1 @ i)) [ (i = 1) -> <k> t x1 @ j /\ k
-                                      , (i = 0) -> <k> g y
-                                      , (j = 0) -> <k> g (p1 @ i) ]
-
-    fill2 : Square A (g y) (g y) x0 x1
+      <i> comp (<k> A) (g y) [ (i = 1) -> rem1, (i = 0) -> rem0 ]
+
+    pfill : Square A (g y) (g y) x0 x1
                      (<k> g y) p rem0 rem1 =
-      <i j> comp (<k> A) (g y) [ (i = 0) -> <k> rem0 @ j /\ k
-                               , (i = 1) -> <k> rem1 @ j /\ k
-                               , (j = 0) -> <k> g y ]
+      <i> fill (<k> A) (g y) [ (i = 1) -> rem1, (i = 0) -> rem0 ]
 
     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 (<k> A) (fill2 @ i @ j) [ (i = 0) -> <k> fill0 @ j @ -k
-                                         , (i = 1) -> <k> fill1 @ j @ -k
+      <i j> comp (<k> A) (pfill @ i @ j) [ (i = 0) -> <k> rem0fill @ j @ -k
+                                         , (i = 1) -> <k> rem1fill @ j @ -k
                                          , (j = 0) -> <k> g y
                                          , (j = 1) -> <k> t (p @ i) @ -k ]
 
-- 
2.34.1