unfolded version of propIsEquivDirect

diff --git a/examples/equiv.ctt b/examples/equiv.ctt
index d4877eb8bd81270794a4277d866adcff109dc332..81d063f5b16f604af7c25777ef20a1390ed01191 100644 (file)
--- a/examples/equiv.ctt
+++ b/examples/equiv.ctt
@@ -37,6 +37,52 @@ propIsEquivDirect (A B : U) (f : A -> B) : prop (isEquiv A B f) =
                                  , (j = 1) -> <k> w ]
           in sq @ i)
 
+-- Unfolded version of propIsEquiv with the same normal form as propIsEquivDirect:
+propIsEquivDirect' (A B : U) (f : A -> B) : prop (isEquiv A B f) =
+  \(p q : isEquiv A B f) ->
+  <i> \(y : B) ->
+    let p0 : A = (p y).1.1
+        p1 : Path B y (f p0) = (p y).1.2
+        p2 : (w1 : fiber A B f y) -> Path (fiber A B f y) (p0,p1) w1 = (p y).2
+        q0 : A = (q y).1.1
+        q1 : Path B y (f q0) = (q y).1.2
+        q2 : (w1 : fiber A B f y) -> Path (fiber A B f y) (q0,q1) w1 = (q y).2
+        alpha : Path (fiber A B f y) (p0,p1) (q0,q1) = p2 (q0,q1)
+    in (alpha @ i,
+        \(w : fiber A B f y) ->
+          let x : A = w.1
+              wx : Path B y (f x) = w.2
+              alpha1 : Path A p0 q0 = <i> (alpha @ i).1
+              alpha2 : PathP (<i> Path B y (f (alpha1 @ i))) p1 q1 =
+                <i> (alpha @ i).2
+              p2w1 : Path A p0 x = <i> (p2 w @ i).1
+              q2w1 : Path A q0 x = <i> (q2 w @ i).1
+              p2w2 : PathP (<i> Path B y (f (p2w1 @ i))) p1 wx = <i> (p2 w @ i).2
+              q2w2 : PathP (<i> Path B y (f (q2w1 @ i))) q1 wx = <i> (q2 w @ i).2
+              sq1 : PathP (<j> Path A (alpha1 @ j) x) p2w1 q2w1 =
+                <i j> comp (<_> A) (p2w1 @ i \/ j)
+                            [ (i = 0) -> <k> p2w1 @ j
+                            , (i = 1) -> <k> q2w1 @ j \/ -k
+                            , (j = 0) -> <k> (p2 (q2 w @ -k) @ i).1
+                            , (j = 1) -> <k> x ]
+
+              -- The l=0 face is f applied to the fill version of sq1, maybe
+              -- compute the filler separately?
+              sq2 : PathP (<i> PathP (<j> Path B y (f (sq1 @ i @ j)))
+                                     (alpha2 @ i) wx)
+                          p2w2 q2w2 =
+                <i j l> comp (<_> B) (p2w2 @ i \/ j @ l)
+                              [ (i = 0) -> <k> p2w2 @ j @ l
+                              , (i = 1) -> <k> q2w2 @ j \/ -k @ l
+                              , (j = 0) -> <k> (p2 (q2 w @ -k) @ i).2 @ l
+                              , (j = 1) -> <k> wx @ l
+                              , (l = 0) -> <k> y
+                              , (l = 1) -> <k> f (fill (<_> A) (p2w1 @ i \/ j)
+                                                        [ (i = 0) -> <k> p2w1 @ j
+                                                        , (i = 1) -> <k> q2w1 @ j \/ -k
+                                                        , (j = 0) -> <k> (p2 (q2 w @ -k) @ i).1
+                                                        , (j = 1) -> <k> x ] @ k) ]
+          in <j> (sq1 @ i @ j,sq2 @ i @ j))
 
 equivLemma (A B : U)
   : (v w : equiv A B) -> Path (A -> B) v.1 w.1 -> Path (equiv A B) v w