From: Anders Mörtberg <andersmortberg@gmail.com>
Date: Sat, 23 Jan 2016 17:51:36 +0000 (-0500)
Subject: cleaning
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=30b6e14f5c9356dfa9bdc52d98d11d60710a2830;p=cubicaltt.git

cleaning
---

diff --git a/Eval.hs b/Eval.hs
index 1bc9055..028789b 100644
--- a/Eval.hs
+++ b/Eval.hs
@@ -274,11 +274,10 @@ v @@ phi                   = error $ "(@@): " ++ show v ++ " should be neutral."
 (VPath i u) @@@ j = u `swap` (i,j)
 v @@@ j           = VAppFormula v (toFormula j)
 
+
 -------------------------------------------------------------------------------
 -- Composition and filling
 
-
-
 comp :: Name -> Val -> Val -> System Val -> Val
 comp i a u ts | eps `member` ts = (ts ! eps) `face` (i ~> 1)
 comp i a u ts = case a of
@@ -431,7 +430,6 @@ transpHIT i a@(Ter (HSum _ _ nass) env) u =
                    VPath j $ transpHIT j (aij `face` alpha) (vAlpha @@ j)) vs
   _ -> error $ "transpHIT: neutral " ++ show u
 
-
 -- given u(i) of type a(i) "squeezeHIT i a u" connects in the direction i
 -- transHIT i a u(i=0) to u(i=1) in a(1)
 squeezeHIT :: Name -> Val -> Val -> Val
@@ -737,8 +735,6 @@ lemEq eq b aps = (a,VPath i (compNeg j (eq @@ j) p1 thetas'))
 --                   insertSystem (i ~> 1) (transFillNeg j ej u) $ ws
 --         theta   = compNeg j ej u xs
 
-
-
 -- Old version:
 -- gradLemmaU :: Val -> Val -> System Val -> Val -> (Val, Val)
 -- gradLemmaU b eq us v = (u, VPath i theta'')
@@ -831,8 +827,8 @@ instance Convertible Val where
       (VHComp a u ts,VHComp a' u' ts')    -> conv ns (a,u,ts) (a',u',ts')
       (VGlue v equivs,VGlue v' equivs')   -> conv ns (v,equivs) (v',equivs')
       (VGlueElem u us,VGlueElem u' us')   -> conv ns (u,us) (u',us')
-      (VUnGlueElemU u _ _,VUnGlueElemU u' _ _) -> conv ns u u'  -- Is this correct?
-      (VUnGlueElem u ts,VUnGlueElem u' ts') -> conv ns (u,ts) (u',ts')
+      (VUnGlueElemU u _ _,VUnGlueElemU u' _ _) -> conv ns u u'
+      (VUnGlueElem u ts,VUnGlueElem u' ts')    -> conv ns (u,ts) (u',ts')
       (VCompU u es,VCompU u' es')              -> conv ns (u,es) (u',es')
       _                                        -> False
 
@@ -893,8 +889,6 @@ instance Normal Val where
     VUnGlueElem u us    -> unglueElem (normal ns u) (normal ns us)
     VUnGlueElemU e u us -> unGlueU (normal ns e) (normal ns u) (normal ns us)
     VCompU a ts         -> VCompU (normal ns a) (normal ns ts)
-    -- TODO: Shouldn't we do:
-    -- VCompU u es         -> compUniv (normal ns u) (normal ns es)
     VVar x t            -> VVar x t -- (normal ns t)
     VFst t              -> fstVal (normal ns t)
     VSnd t              -> sndVal (normal ns t)
diff --git a/examples/bool.ctt b/examples/bool.ctt
index a101367..5edda04 100644
--- a/examples/bool.ctt
+++ b/examples/bool.ctt
@@ -170,3 +170,23 @@ eqBool : Id U bool bool =
 
 testf : bool = trans bool bool eqBool true
 testt : bool = trans bool bool eqBool false
+
+-- Some tests of normal forms of univalence:
+testUniv1 (A : U) : Id U A A =
+  trans (equiv A A) (Id U A A) (<i> corrUniv A A @ -i) (idEquiv A)
+
+-- obtained by normal form
+ntestUniv1 (A:U) : Id U A A =
+ <i> comp (<_>U)
+      (comp (<_>U) A
+         [ (i = 0) -> <l> comp (<_>U) A [ (l = 0) -> <i> glue A [ (i = 0) -> (A,(\(x : A) -> x,\(a : A) -> ((a,<l> a),\(z : ((x : A) * IdP (<l> A) a x)) -> <l> (z.2 @ l,<i> z.2 @ (l /\ i))))), (i = 1) -> (A,(comp (<l> A -> A) (\(x : A) -> x) [],comp (<l> (y : A) ->
+  ((x : ((x : A) * IdP (<j> A) y (comp (<j> A) (comp (<i> A) x []) [ (l = 0) -> <j> comp (<k> A) x [ (j = 1) -> <k> x ] ]))) *    (y0 : ((x0 : A) * IdP (<j> A) y (comp (<j> A) (comp (<i> A) x0 []) [ (l = 0) -> <j> comp (<k> A) x0 [ (j = 1) -> <k> x0 ] ]))) -> IdP (<j> ((x0 : A) * IdP (<j> A) y (comp (<j> A) (comp (<i> A) x0 []) [ (l = 0) -> <j> comp (<k> A) x0 [ (j = 1) -> <k> x0 ] ]))) x y0)) (\(a : A) -> ((a,<l> a),\(z : ((x : A) * IdP (<l> A) a x)) -> <l> (z.2 @ l,<i> z.2 @ (l /\ i)))) [])) ], (l = 1) -> <i> glue A [ (i = 0) -> (A,(\(x : A) -> x,\(a : A) -> ((a,<l> a),\(z : ((x : A) * IdP (<l> A) a x)) -> <l> (z.2 @ l,<i> z.2 @ (l /\ i))))), (i = 1) -> (A,(comp (<l> A -> A) (\(x : A) -> x) [],comp (<l> (y : A) ->
+        ((x : ((x : A) * IdP (<j> A) y (comp (<j> A) (comp (<i> A) x []) [ (l = 0) -> <j> comp (<k> A) x [ (j = 1) -> <k> x ] ]))) * (y0 : ((x0 : A) * IdP (<j> A) y (comp (<j> A) (comp (<i> A) x0 []) [ (l = 0) -> <j> comp (<k> A) x0 [ (j = 1) -> <k> x0 ] ]))) -> IdP (<j> ((x0 : A) * IdP (<j> A) y (comp (<j> A) (comp (<i> A) x0 []) [ (l = 0) -> <j> comp (<k> A) x0 [ (j = 1) -> <k> x0 ] ]))) x y0)) (\(a : A) -> ((a,<l> a),\(z : ((x : A) * IdP (<l> A) a x)) -> <l> (z.2 @ l,<i> z.2 @ (l /\ i)))) [])) ] ], (i = 1) -> <l> A ]) [ (i = 0) -> <l> A, (i = 1) -> <l> A ]
+
+testUniv2 : bool = trans bool bool (ntestUniv1 bool) true
+
+ntestUniv2 : bool =
+ comp (<i> comp (<_>U) (comp (<_>U) bool [ (i = 0) -> <j> comp (<_>U) bool [ (j = 0) -> <i> glue bool [ (i = 0) -> (bool,(\(x : bool) -> x,\(a : bool) -> ((a,<i> a),\(z : ((x : bool) * IdP (<i> bool) a x)) -> <i> (z.2 @ i,<j> z.2 @ (i /\ j))))), (i = 1) -> (bool,(comp (<i> bool -> bool) (\(x : bool) -> x) [],comp (<i> (y : bool) ->
+  ((x : ((x : bool) * IdP (<j> bool) y (comp (<j> bool) (comp (<i> bool) x []) [ (i = 0) -> <j> comp (<k> bool) x [ (j = 1) -> <k> x ] ]))) * (y0 : ((x0 : bool) * IdP (<j> bool) y (comp (<j> bool) (comp (<i> bool) x0 []) [ (i = 0) -> <j> comp (<k> bool) x0 [ (j = 1) -> <k> x0 ] ]))) -> IdP (<j> ((x0 : bool) * IdP (<k> bool) y (comp (<j> bool) (comp (<i> bool) x0 []) [ (i = 0) -> <j> comp (<k> bool) x0 [ (j = 1) -> <k> x0 ] ]))) x y0)) (\(a : bool) -> ((a,<i> a),\(z : ((x : bool) * IdP (<i> bool) a x)) -> <i> (z.2 @ i,<j> z.2 @ (i /\ j)))) [])) ], (j = 1) -> <i> glue bool [ (i = 0) -> (bool,(\(x : bool) -> x,\(a : bool) -> ((a,<i> a),\(z : ((x : bool) * IdP (<i> bool) a x)) -> <i> (z.2 @ i,<j> z.2 @ (i /\ j))))), (i = 1) -> (bool,(comp (<i> bool -> bool) (\(x : bool) -> x) [],comp (<i> (y : bool) ->
+  ((x : ((x : bool) * IdP (<j> bool) y (comp (<j> bool) (comp (<i> bool) x []) [ (i = 0) -> <j> comp (<k> bool) x [ (j = 1) -> <k> x ] ]))) * (y0 : ((x0 : bool) * IdP (<j> bool) y (comp (<j> bool) (comp (<i> bool) x0 []) [ (i = 0) -> <j> comp (<k> bool) x0 [ (j = 1) -> <k> x0 ] ]))) -> IdP (<j> ((x0 : bool) * IdP (<k> bool) y (comp (<j> bool) (comp (<i> bool) x0 []) [ (i = 0) -> <j> comp (<k> bool) x0 [ (j = 1) -> <k> x0 ] ]))) x y0)) (\(a : bool) -> ((a,<i> a),\(z : ((x : bool) * IdP (<i> bool) a x)) -> <i> (z.2 @ i,<j> z.2 @ (i /\ j)))) [])) ] ], (i = 1) -> <j> bool ]) [ (i = 0) -> <j> bool, (i = 1) -> <j> bool ]) true []
+
diff --git a/examples/hz.ctt b/examples/hz.ctt
index a2d5261..782b58c 100644
--- a/examples/hz.ctt
+++ b/examples/hz.ctt
@@ -1,3 +1,5 @@
+-- Z defined as a quotient of nat * nat by the relation: 
+--   (x1,x2) ~ (y1,y2) := (x1 + y2 = x2 + y1)
 module hz where
 
 import nat
@@ -58,5 +60,8 @@ discretehz : discrete hz = isdiscretesetquot nat2 rel rem
   rem (x y : nat2) : isdecprop (rel.1 x y).1 = 
     (natSet (add x.1 y.2) (add x.2 y.1),natDec (add x.1 y.2) (add x.2 y.1))
 
+-- Use the decision procedure to compute if "0 = 1":
 test01 : bool = discretetobool hz discretehz zeroz onez
+
+-- Use the decision procedure to compute if "1 = 1":
 test11 : bool = discretetobool hz discretehz onez onez
\ No newline at end of file
diff --git a/examples/setquot.ctt b/examples/setquot.ctt
index 3661e1f..e0fe8f2 100644
--- a/examples/setquot.ctt
+++ b/examples/setquot.ctt
@@ -1,3 +1,4 @@
+-- Formalization of (impredicative) set quotients
 module setquot where
 
 import bool
diff --git a/examples/univalence.ctt b/examples/univalence.ctt
index 697a388..2ed8ee2 100644
--- a/examples/univalence.ctt
+++ b/examples/univalence.ctt
@@ -1,8 +1,8 @@
 -- This file contains two proofs of the univalence axiom. One using
 -- unglue (section 7.2) and a direct one (appendix B of the cubicaltt
--- paper). The normal form of the first proof can be computed while
--- the second one uses very much memory and don't terminate in
--- reasonable time.
+-- paper). The normal form of the first proof can be computed (and
+-- typecheck, see nthmUniv) while the second one uses very much memory
+-- and don't terminate in reasonable time.
 module univalence where
 
 import equiv
@@ -77,7 +77,7 @@ equivFunFib (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (cB : isContr (Sigma A
                          (isEquivContr (Sigma A B) (Sigma A C) cB cC (totalFun A B C f) (x,z))
 
 -- test normal form
--- nequivFunFib : (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (cB : isContr (Sigma A B)) (cC : isContr (Sigma A C)) (x:A) ->isEquiv (B x) (C x) (f x) = \(A : U) -> \(B C : A -> U) -> \(f : (x : A) -> (B x) -> (C x)) -> \(cB : Sigma (Sigma A (\(x : A) -> B x)) (\(x : Sigma A (\(x : A) -> B x)) -> (y : Sigma A (\(x0 : A) -> B x0)) -> IdP (<!0> Sigma A (\(x0 : A) -> B x0)) x y)) -> \(cC : Sigma (Sigma A (\(x : A) -> C x)) (\(x : Sigma A (\(x : A) -> C x)) -> (y : Sigma A (\(x0 : A) -> C x0)) -> IdP (<!0> Sigma A (\(x0 : A) -> C x0)) x y)) -> \(x : A) -> \(z : C x) -> ((comp (<!0> B (comp (<!1> A) cC.1.1 [ (!0 = 0) -> <!1> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !1).1, (!0 = 1) -> <!1> (cC.2 ((x,z)) @ !1).1 ])) cB.1.2 [],<!0> comp (<!1> C (comp (<!2> A) cC.1.1 [ (!0 = 0) -> <!2> (cC.2 ((x,z)) @ !2).1, (!0 = 1)(!1 = 0) -> <!2> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !2).1, (!1 = 1) -> <!2> (cC.2 ((x,z)) @ !2).1 ])) (comp (<!1> C (comp (<!2> A) cC.1.1 [ (!0 = 0) -> <!2> (cC.2 ((x,z)) @ (!1 /\ !2)).1, (!0 = 1) -> <!2> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!1 /\ !2)).1, (!1 = 0) -> <!2> cC.1.1 ])) cC.1.2 [ (!0 = 0) -> <!1> (cC.2 ((x,z)) @ !1).2, (!0 = 1) -> <!1> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !1).2 ]) [ (!0 = 0) -> <!1> z, (!0 = 1) -> <!1> f (comp (<!2> A) cC.1.1 [ (!1 = 0) -> <!2> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !2).1, (!1 = 1) -> <!2> (cC.2 ((x,z)) @ !2).1 ]) (comp (<!2> B (comp (<!3> A) cC.1.1 [ (!1 = 0) -> <!3> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !3).1, (!1 = 1)(!2 = 1) -> <!3> (cC.2 ((x,z)) @ !3).1, (!2 = 0) -> <!3> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !3).1 ])) cB.1.2 [ (!1 = 0) -> <!2> cB.1.2 ]) ]),\(x0 : Sigma (B x) (\(x0 : B x) -> IdP (<!0> C x) z (f x x0))) -> <!0> (comp (<!1> B x) (comp (<!1> B (comp (<!2> A) cC.1.1 [ (!0 = 0) -> <!2> comp (<!3> A) cC.1.1 [ (!1 = 0) -> <!3> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!2 /\ !3)).1, (!1 = 1) -> <!3> (cC.2 ((x,z)) @ (!2 /\ !3)).1, (!2 = 0) -> <!3> cC.1.1 ], (!0 = 1) -> <!2> (cC.2 ((x,x0.2 @ -!1)) @ !2).1, (!1 = 0) -> <!2> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !2).1, (!1 = 1) -> <!2> (cC.2 ((x,z)) @ !2).1 ])) (cB.2 ((x,x0.1)) @ !0).2 []) [ (!0 = 0) -> <!1> comp (<!0> B (comp (<!1> A) cC.1.1 [ (!0 = 0) -> <!1> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !1).1, (!0 = 1) -> <!1> (cC.2 ((x,z)) @ !1).1 ])) cB.1.2 [], (!0 = 1) -> <!1> comp (<!2> B x) x0.1 [ (!1 = 1) -> <!2> x0.1 ] ],<!2> comp (<!3> C x) (comp (<!3> C (comp (<!4> A) cC.1.1 [ (!0 = 0) -> <!4> comp (<!5> A) cC.1.1 [ (!2 = 0) -> <!5> (cC.2 ((x,z)) @ (!4 /\ !5)).1, (!2 = 1)(!3 = 0) -> <!5> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!4 /\ !5)).1, (!3 = 1) -> <!5> (cC.2 ((x,z)) @ (!4 /\ !5)).1, (!4 = 0) -> <!5> cC.1.1 ], (!0 = 1) -> <!4> (cC.2 ((x,x0.2 @ (!2 /\ -!3))) @ !4).1, (!2 = 0) -> <!4> (cC.2 ((x,z)) @ !4).1, (!2 = 1)(!3 = 0) -> <!4> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !4).1, (!3 = 1) -> <!4> (cC.2 ((x,z)) @ !4).1 ])) (comp (<!3> C (comp (<!4> A) cC.1.1 [ (!0 = 0) -> <!4> comp (<!5> A) cC.1.1 [ (!2 = 0) -> <!5> (cC.2 ((x,z)) @ (!3 /\ !4 /\ !5)).1, (!2 = 1) -> <!5> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!3 /\ !4 /\ !5)).1, (!3 = 0) -> <!5> cC.1.1, (!4 = 0) -> <!5> cC.1.1 ], (!0 = 1) -> <!4> (cC.2 ((x,x0.2 @ !2)) @ (!3 /\ !4)).1, (!2 = 0) -> <!4> (cC.2 ((x,z)) @ (!3 /\ !4)).1, (!2 = 1) -> <!4> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ (!3 /\ !4)).1, (!3 = 0) -> <!4> cC.1.1 ])) cC.1.2 [ (!0 = 0) -> <!3> comp (<!4> C (comp (<!5> A) cC.1.1 [ (!2 = 0) -> <!5> (cC.2 ((x,z)) @ (!3 /\ !4 /\ !5)).1, (!2 = 1) -> <!5> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!3 /\ !4 /\ !5)).1, (!3 = 0) -> <!5> cC.1.1, (!4 = 0) -> <!5> cC.1.1 ])) cC.1.2 [ (!2 = 0) -> <!4> (cC.2 ((x,z)) @ (!3 /\ !4)).2, (!2 = 1) -> <!4> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!3 /\ !4)).2, (!3 = 0) -> <!4> cC.1.2 ], (!0 = 1) -> <!3> (cC.2 ((x,x0.2 @ !2)) @ !3).2, (!2 = 0) -> <!3> (cC.2 ((x,z)) @ !3).2, (!2 = 1) -> <!3> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !3).2 ]) [ (!2 = 0) -> <!3> z, (!2 = 1) -> <!3> f (comp (<!4> A) cC.1.1 [ (!0 = 0) -> <!4> comp (<!5> A) cC.1.1 [ (!3 = 0) -> <!5> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!4 /\ !5)).1, (!3 = 1) -> <!5> (cC.2 ((x,z)) @ (!4 /\ !5)).1, (!4 = 0) -> <!5> cC.1.1 ], (!0 = 1) -> <!4> (cC.2 ((x,x0.2 @ -!3)) @ !4).1, (!3 = 0) -> <!4> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !4).1, (!3 = 1) -> <!4> (cC.2 ((x,z)) @ !4).1 ]) (comp (<!4> B (comp (<!5> A) cC.1.1 [ (!0 = 0) -> <!5> comp (<!6> A) cC.1.1 [ (!3 = 0) -> <!6> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!5 /\ !6)).1, (!3 = 1)(!4 = 1) -> <!6> (cC.2 ((x,z)) @ (!5 /\ !6)).1, (!4 = 0) -> <!6> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!5 /\ !6)).1, (!5 = 0) -> <!6> cC.1.1 ], (!0 = 1) -> <!5> (cC.2 ((x,x0.2 @ (-!3 \/ -!4))) @ !5).1, (!3 = 0) -> <!5> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !5).1, (!3 = 1)(!4 = 1) -> <!5> (cC.2 ((x,z)) @ !5).1, (!4 = 0) -> <!5> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !5).1 ])) (cB.2 ((x,x0.1)) @ !0).2 [ (!3 = 0) -> <!4> (cB.2 ((x,x0.1)) @ !0).2 ]) ]) [ (!0 = 0) -> <!3> comp (<!3> C (comp (<!4> A) cC.1.1 [ (!2 = 0) -> <!4> (cC.2 ((x,z)) @ !4).1, (!2 = 1)(!3 = 0) -> <!4> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !4).1, (!3 = 1) -> <!4> (cC.2 ((x,z)) @ !4).1 ])) (comp (<!3> C (comp (<!4> A) cC.1.1 [ (!2 = 0) -> <!4> (cC.2 ((x,z)) @ (!3 /\ !4)).1, (!2 = 1) -> <!4> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!3 /\ !4)).1, (!3 = 0) -> <!4> cC.1.1 ])) cC.1.2 [ (!2 = 0) -> <!3> (cC.2 ((x,z)) @ !3).2, (!2 = 1) -> <!3> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !3).2 ]) [ (!2 = 0) -> <!3> z, (!2 = 1) -> <!3> f (comp (<!4> A) cC.1.1 [ (!3 = 0) -> <!4> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !4).1, (!3 = 1) -> <!4> (cC.2 ((x,z)) @ !4).1 ]) (comp (<!4> B (comp (<!5> A) cC.1.1 [ (!3 = 0) -> <!5> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !5).1, (!3 = 1)(!4 = 1) -> <!5> (cC.2 ((x,z)) @ !5).1, (!4 = 0) -> <!5> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !5).1 ])) cB.1.2 [ (!3 = 0) -> <!4> cB.1.2 ]) ], (!0 = 1) -> <!3> comp (<!4> C x) (x0.2 @ !2) [ (!2 = 0) -> <!4> z, (!2 = 1) -> <!4> f x (comp (<!5> B x) x0.1 [ (!3 = 1) -> <!5> x0.1, (!4 = 0) -> <!5> x0.1 ]), (!3 = 1) -> <!4> x0.2 @ !2 ], (!2 = 0) -> <!3> z, (!2 = 1) -> <!3> f x (comp (<!4> B x) (comp (<!1> B (comp (<!2> A) cC.1.1 [ (!0 = 0) -> <!2> comp (<!3> A) cC.1.1 [ (!1 = 0) -> <!3> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!2 /\ !3)).1, (!1 = 1) -> <!3> (cC.2 ((x,z)) @ (!2 /\ !3)).1, (!2 = 0) -> <!3> cC.1.1 ], (!0 = 1) -> <!2> (cC.2 ((x,x0.2 @ -!1)) @ !2).1, (!1 = 0) -> <!2> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !2).1, (!1 = 1) -> <!2> (cC.2 ((x,z)) @ !2).1 ])) (cB.2 ((x,x0.1)) @ !0).2 []) [ (!0 = 0) -> <!4> comp (<!0> B (comp (<!1> A) cC.1.1 [ (!0 = 0) -> <!1> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !1).1, (!0 = 1) -> <!1> (cC.2 ((x,z)) @ !1).1 ])) cB.1.2 [], (!0 = 1) -> <!4> comp (<!5> B x) x0.1 [ (!3 = 1)(!4 = 1) -> <!5> x0.1 ], (!3 = 0) -> <!4> comp (<!1> B (comp (<!2> A) cC.1.1 [ (!0 = 0) -> <!2> comp (<!3> A) cC.1.1 [ (!1 = 0) -> <!3> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!2 /\ !3)).1, (!1 = 1) -> <!3> (cC.2 ((x,z)) @ (!2 /\ !3)).1, (!2 = 0) -> <!3> cC.1.1 ], (!0 = 1) -> <!2> (cC.2 ((x,x0.2 @ -!1)) @ !2).1, (!1 = 0) -> <!2> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !2).1, (!1 = 1) -> <!2> (cC.2 ((x,z)) @ !2).1 ])) (cB.2 ((x,x0.1)) @ !0).2 [] ]) ]))
+nequivFunFib : (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (cB : isContr (Sigma A B)) (cC : isContr (Sigma A C)) (x:A) ->isEquiv (B x) (C x) (f x) = \(A : U) -> \(B C : A -> U) -> \(f : (x : A) -> (B x) -> (C x)) -> \(cB : Sigma (Sigma A (\(x : A) -> B x)) (\(x : Sigma A (\(x : A) -> B x)) -> (y : Sigma A (\(x0 : A) -> B x0)) -> IdP (<!0> Sigma A (\(x0 : A) -> B x0)) x y)) -> \(cC : Sigma (Sigma A (\(x : A) -> C x)) (\(x : Sigma A (\(x : A) -> C x)) -> (y : Sigma A (\(x0 : A) -> C x0)) -> IdP (<!0> Sigma A (\(x0 : A) -> C x0)) x y)) -> \(x : A) -> \(z : C x) -> ((comp (<!0> B (comp (<!1> A) cC.1.1 [ (!0 = 0) -> <!1> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !1).1, (!0 = 1) -> <!1> (cC.2 ((x,z)) @ !1).1 ])) cB.1.2 [],<!0> comp (<!1> C (comp (<!2> A) cC.1.1 [ (!0 = 0) -> <!2> (cC.2 ((x,z)) @ !2).1, (!0 = 1)(!1 = 0) -> <!2> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !2).1, (!1 = 1) -> <!2> (cC.2 ((x,z)) @ !2).1 ])) (comp (<!1> C (comp (<!2> A) cC.1.1 [ (!0 = 0) -> <!2> (cC.2 ((x,z)) @ (!1 /\ !2)).1, (!0 = 1) -> <!2> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!1 /\ !2)).1, (!1 = 0) -> <!2> cC.1.1 ])) cC.1.2 [ (!0 = 0) -> <!1> (cC.2 ((x,z)) @ !1).2, (!0 = 1) -> <!1> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !1).2 ]) [ (!0 = 0) -> <!1> z, (!0 = 1) -> <!1> f (comp (<!2> A) cC.1.1 [ (!1 = 0) -> <!2> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !2).1, (!1 = 1) -> <!2> (cC.2 ((x,z)) @ !2).1 ]) (comp (<!2> B (comp (<!3> A) cC.1.1 [ (!1 = 0) -> <!3> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !3).1, (!1 = 1)(!2 = 1) -> <!3> (cC.2 ((x,z)) @ !3).1, (!2 = 0) -> <!3> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !3).1 ])) cB.1.2 [ (!1 = 0) -> <!2> cB.1.2 ]) ]),\(x0 : Sigma (B x) (\(x0 : B x) -> IdP (<!0> C x) z (f x x0))) -> <!0> (comp (<!1> B x) (comp (<!1> B (comp (<!2> A) cC.1.1 [ (!0 = 0) -> <!2> comp (<!3> A) cC.1.1 [ (!1 = 0) -> <!3> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!2 /\ !3)).1, (!1 = 1) -> <!3> (cC.2 ((x,z)) @ (!2 /\ !3)).1, (!2 = 0) -> <!3> cC.1.1 ], (!0 = 1) -> <!2> (cC.2 ((x,x0.2 @ -!1)) @ !2).1, (!1 = 0) -> <!2> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !2).1, (!1 = 1) -> <!2> (cC.2 ((x,z)) @ !2).1 ])) (cB.2 ((x,x0.1)) @ !0).2 []) [ (!0 = 0) -> <!1> comp (<!0> B (comp (<!1> A) cC.1.1 [ (!0 = 0) -> <!1> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !1).1, (!0 = 1) -> <!1> (cC.2 ((x,z)) @ !1).1 ])) cB.1.2 [], (!0 = 1) -> <!1> comp (<!2> B x) x0.1 [ (!1 = 1) -> <!2> x0.1 ] ],<!2> comp (<!3> C x) (comp (<!3> C (comp (<!4> A) cC.1.1 [ (!0 = 0) -> <!4> comp (<!5> A) cC.1.1 [ (!2 = 0) -> <!5> (cC.2 ((x,z)) @ (!4 /\ !5)).1, (!2 = 1)(!3 = 0) -> <!5> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!4 /\ !5)).1, (!3 = 1) -> <!5> (cC.2 ((x,z)) @ (!4 /\ !5)).1, (!4 = 0) -> <!5> cC.1.1 ], (!0 = 1) -> <!4> (cC.2 ((x,x0.2 @ (!2 /\ -!3))) @ !4).1, (!2 = 0) -> <!4> (cC.2 ((x,z)) @ !4).1, (!2 = 1)(!3 = 0) -> <!4> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !4).1, (!3 = 1) -> <!4> (cC.2 ((x,z)) @ !4).1 ])) (comp (<!3> C (comp (<!4> A) cC.1.1 [ (!0 = 0) -> <!4> comp (<!5> A) cC.1.1 [ (!2 = 0) -> <!5> (cC.2 ((x,z)) @ (!3 /\ !4 /\ !5)).1, (!2 = 1) -> <!5> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!3 /\ !4 /\ !5)).1, (!3 = 0) -> <!5> cC.1.1, (!4 = 0) -> <!5> cC.1.1 ], (!0 = 1) -> <!4> (cC.2 ((x,x0.2 @ !2)) @ (!3 /\ !4)).1, (!2 = 0) -> <!4> (cC.2 ((x,z)) @ (!3 /\ !4)).1, (!2 = 1) -> <!4> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ (!3 /\ !4)).1, (!3 = 0) -> <!4> cC.1.1 ])) cC.1.2 [ (!0 = 0) -> <!3> comp (<!4> C (comp (<!5> A) cC.1.1 [ (!2 = 0) -> <!5> (cC.2 ((x,z)) @ (!3 /\ !4 /\ !5)).1, (!2 = 1) -> <!5> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!3 /\ !4 /\ !5)).1, (!3 = 0) -> <!5> cC.1.1, (!4 = 0) -> <!5> cC.1.1 ])) cC.1.2 [ (!2 = 0) -> <!4> (cC.2 ((x,z)) @ (!3 /\ !4)).2, (!2 = 1) -> <!4> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!3 /\ !4)).2, (!3 = 0) -> <!4> cC.1.2 ], (!0 = 1) -> <!3> (cC.2 ((x,x0.2 @ !2)) @ !3).2, (!2 = 0) -> <!3> (cC.2 ((x,z)) @ !3).2, (!2 = 1) -> <!3> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !3).2 ]) [ (!2 = 0) -> <!3> z, (!2 = 1) -> <!3> f (comp (<!4> A) cC.1.1 [ (!0 = 0) -> <!4> comp (<!5> A) cC.1.1 [ (!3 = 0) -> <!5> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!4 /\ !5)).1, (!3 = 1) -> <!5> (cC.2 ((x,z)) @ (!4 /\ !5)).1, (!4 = 0) -> <!5> cC.1.1 ], (!0 = 1) -> <!4> (cC.2 ((x,x0.2 @ -!3)) @ !4).1, (!3 = 0) -> <!4> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !4).1, (!3 = 1) -> <!4> (cC.2 ((x,z)) @ !4).1 ]) (comp (<!4> B (comp (<!5> A) cC.1.1 [ (!0 = 0) -> <!5> comp (<!6> A) cC.1.1 [ (!3 = 0) -> <!6> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!5 /\ !6)).1, (!3 = 1)(!4 = 1) -> <!6> (cC.2 ((x,z)) @ (!5 /\ !6)).1, (!4 = 0) -> <!6> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!5 /\ !6)).1, (!5 = 0) -> <!6> cC.1.1 ], (!0 = 1) -> <!5> (cC.2 ((x,x0.2 @ (-!3 \/ -!4))) @ !5).1, (!3 = 0) -> <!5> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !5).1, (!3 = 1)(!4 = 1) -> <!5> (cC.2 ((x,z)) @ !5).1, (!4 = 0) -> <!5> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !5).1 ])) (cB.2 ((x,x0.1)) @ !0).2 [ (!3 = 0) -> <!4> (cB.2 ((x,x0.1)) @ !0).2 ]) ]) [ (!0 = 0) -> <!3> comp (<!3> C (comp (<!4> A) cC.1.1 [ (!2 = 0) -> <!4> (cC.2 ((x,z)) @ !4).1, (!2 = 1)(!3 = 0) -> <!4> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !4).1, (!3 = 1) -> <!4> (cC.2 ((x,z)) @ !4).1 ])) (comp (<!3> C (comp (<!4> A) cC.1.1 [ (!2 = 0) -> <!4> (cC.2 ((x,z)) @ (!3 /\ !4)).1, (!2 = 1) -> <!4> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!3 /\ !4)).1, (!3 = 0) -> <!4> cC.1.1 ])) cC.1.2 [ (!2 = 0) -> <!3> (cC.2 ((x,z)) @ !3).2, (!2 = 1) -> <!3> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !3).2 ]) [ (!2 = 0) -> <!3> z, (!2 = 1) -> <!3> f (comp (<!4> A) cC.1.1 [ (!3 = 0) -> <!4> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !4).1, (!3 = 1) -> <!4> (cC.2 ((x,z)) @ !4).1 ]) (comp (<!4> B (comp (<!5> A) cC.1.1 [ (!3 = 0) -> <!5> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !5).1, (!3 = 1)(!4 = 1) -> <!5> (cC.2 ((x,z)) @ !5).1, (!4 = 0) -> <!5> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !5).1 ])) cB.1.2 [ (!3 = 0) -> <!4> cB.1.2 ]) ], (!0 = 1) -> <!3> comp (<!4> C x) (x0.2 @ !2) [ (!2 = 0) -> <!4> z, (!2 = 1) -> <!4> f x (comp (<!5> B x) x0.1 [ (!3 = 1) -> <!5> x0.1, (!4 = 0) -> <!5> x0.1 ]), (!3 = 1) -> <!4> x0.2 @ !2 ], (!2 = 0) -> <!3> z, (!2 = 1) -> <!3> f x (comp (<!4> B x) (comp (<!1> B (comp (<!2> A) cC.1.1 [ (!0 = 0) -> <!2> comp (<!3> A) cC.1.1 [ (!1 = 0) -> <!3> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!2 /\ !3)).1, (!1 = 1) -> <!3> (cC.2 ((x,z)) @ (!2 /\ !3)).1, (!2 = 0) -> <!3> cC.1.1 ], (!0 = 1) -> <!2> (cC.2 ((x,x0.2 @ -!1)) @ !2).1, (!1 = 0) -> <!2> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !2).1, (!1 = 1) -> <!2> (cC.2 ((x,z)) @ !2).1 ])) (cB.2 ((x,x0.1)) @ !0).2 []) [ (!0 = 0) -> <!4> comp (<!0> B (comp (<!1> A) cC.1.1 [ (!0 = 0) -> <!1> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !1).1, (!0 = 1) -> <!1> (cC.2 ((x,z)) @ !1).1 ])) cB.1.2 [], (!0 = 1) -> <!4> comp (<!5> B x) x0.1 [ (!3 = 1)(!4 = 1) -> <!5> x0.1 ], (!3 = 0) -> <!4> comp (<!1> B (comp (<!2> A) cC.1.1 [ (!0 = 0) -> <!2> comp (<!3> A) cC.1.1 [ (!1 = 0) -> <!3> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!2 /\ !3)).1, (!1 = 1) -> <!3> (cC.2 ((x,z)) @ (!2 /\ !3)).1, (!2 = 0) -> <!3> cC.1.1 ], (!0 = 1) -> <!2> (cC.2 ((x,x0.2 @ -!1)) @ !2).1, (!1 = 0) -> <!2> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !2).1, (!1 = 1) -> <!2> (cC.2 ((x,z)) @ !2).1 ])) (cB.2 ((x,x0.1)) @ !0).2 [] ]) ]))
 
 
 lem1 (B:U) : isContr ((X:U) * equiv X B) =
@@ -114,7 +114,7 @@ lem1 (B:U) : isContr ((X:U) * equiv X B) =
                                                   ,(j=1) -> v.2])
                   in (center,contr)))
 
--- nlem1 (B:U) : isContr ((X:U) * equiv X B) = ((B,(\(x : B) -> x,\(a : B) -> ((a,<!0> a),\(z : Sigma B (\(x : B) -> IdP (<!0> B) a x)) -> <!0> (z.2 @ !0,<!1> z.2 @ (!0 /\ !1))))),\(w : Sigma U (\(X : U) -> Sigma (X -> B) (\(f : X -> B) -> (y : B) -> Sigma (Sigma X (\(x : X) -> IdP (<!0> B) y (f x))) (\(x : Sigma X (\(x : X) -> IdP (<!0> B) y (f x))) -> (y0 : Sigma X (\(x0 : X) -> IdP (<!0> B) y (f x0))) -> IdP (<!0> Sigma X (\(x0 : X) -> IdP (<!0> B) y (f x0))) x y0)))) -> <!0> (glue B [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a,<!0> a),\(z : Sigma B (\(x : B) -> IdP (<!0> B) a x)) -> <!0> (z.2 @ !0,<!1> z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ],(\(g : glue B [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a,<!0> a),\(z : Sigma B (\(x : B) -> IdP (<!0> B) a x)) -> <!0> (z.2 @ !0,<!1> z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ]) -> unglueElem g [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a,<!0> a),\(z : Sigma B (\(x : B) -> IdP (<!0> B) a x)) -> <!0> (z.2 @ !0,<!1> z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ],\(b : B) -> ((glueElem (comp (<!1> B) b [ (!0 = 0) -> <!1> b, (!0 = 1) -> <!1> (w.2.2 b).1.2 @ !1 ]) [ (!0 = 0) -> b, (!0 = 1) -> (w.2.2 b).1.1 ],<!1> comp (<!2> B) b [ (!0 = 0) -> <!2> b, (!0 = 1) -> <!2> (w.2.2 b).1.2 @ (!1 /\ !2), (!1 = 0) -> <!2> b ]),\(v : Sigma (glue B [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a,<!0> a),\(z : Sigma B (\(x : B) -> IdP (<!0> B) a x)) -> <!0> (z.2 @ !0,<!1> z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ]) (\(x : glue B [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a,<!0> a),\(z : Sigma B (\(x : B) -> IdP (<!0> B) a x)) -> <!0> (z.2 @ !0,<!1> z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ]) -> IdP (<!1> B) b (unglueElem x [ (!0 = 0) -> (B,(\(x0 : B) -> x0,\(a : B) -> ((a,<!0> a),\(z : Sigma B (\(x0 : B) -> IdP (<!0> B) a x0)) -> <!0> (z.2 @ !0,<!1> z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ]))) -> <!1> (glueElem (comp (<!2> B) b [ (!0 = 0) -> <!2> v.2 @ (!1 /\ !2), (!0 = 1) -> <!2> ((w.2.2 b).2 v @ !1).2 @ !2, (!1 = 0) -> <!2> comp (<!3> B) b [ (!0 = 0) -> <!3> b, (!0 = 1) -> <!3> (w.2.2 b).1.2 @ (!2 /\ !3), (!2 = 0) -> <!3> b ], (!1 = 1) -> <!2> v.2 @ !2 ]) [ (!0 = 0) -> v.2 @ !1, (!0 = 1) -> ((w.2.2 b).2 v @ !1).1 ],<!2> comp (<!3> B) b [ (!0 = 0) -> <!3> v.2 @ (!1 /\ !2 /\ !3), (!0 = 1) -> <!3> ((w.2.2 b).2 v @ !1).2 @ (!2 /\ !3), (!1 = 0) -> <!3> comp (<!4> B) b [ (!0 = 0) -> <!4> b, (!0 = 1) -> <!4> (w.2.2 b).1.2 @ (!2 /\ !3 /\ !4), (!2 = 0) -> <!4> b, (!3 = 0) -> <!4> b ], (!1 = 1) -> <!3> v.2 @ (!2 /\ !3), (!2 = 0) -> <!3> b ])))))
+nlem1 (B:U) : isContr ((X:U) * equiv X B) = ((B,(\(x : B) -> x,\(a : B) -> ((a,<!0> a),\(z : Sigma B (\(x : B) -> IdP (<!0> B) a x)) -> <!0> (z.2 @ !0,<!1> z.2 @ (!0 /\ !1))))),\(w : Sigma U (\(X : U) -> Sigma (X -> B) (\(f : X -> B) -> (y : B) -> Sigma (Sigma X (\(x : X) -> IdP (<!0> B) y (f x))) (\(x : Sigma X (\(x : X) -> IdP (<!0> B) y (f x))) -> (y0 : Sigma X (\(x0 : X) -> IdP (<!0> B) y (f x0))) -> IdP (<!0> Sigma X (\(x0 : X) -> IdP (<!0> B) y (f x0))) x y0)))) -> <!0> (glue B [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a,<!0> a),\(z : Sigma B (\(x : B) -> IdP (<!0> B) a x)) -> <!0> (z.2 @ !0,<!1> z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ],(\(g : glue B [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a,<!0> a),\(z : Sigma B (\(x : B) -> IdP (<!0> B) a x)) -> <!0> (z.2 @ !0,<!1> z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ]) -> unglueElem g [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a,<!0> a),\(z : Sigma B (\(x : B) -> IdP (<!0> B) a x)) -> <!0> (z.2 @ !0,<!1> z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ],\(b : B) -> ((glueElem (comp (<!1> B) b [ (!0 = 0) -> <!1> b, (!0 = 1) -> <!1> (w.2.2 b).1.2 @ !1 ]) [ (!0 = 0) -> b, (!0 = 1) -> (w.2.2 b).1.1 ],<!1> comp (<!2> B) b [ (!0 = 0) -> <!2> b, (!0 = 1) -> <!2> (w.2.2 b).1.2 @ (!1 /\ !2), (!1 = 0) -> <!2> b ]),\(v : Sigma (glue B [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a,<!0> a),\(z : Sigma B (\(x : B) -> IdP (<!0> B) a x)) -> <!0> (z.2 @ !0,<!1> z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ]) (\(x : glue B [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a,<!0> a),\(z : Sigma B (\(x : B) -> IdP (<!0> B) a x)) -> <!0> (z.2 @ !0,<!1> z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ]) -> IdP (<!1> B) b (unglueElem x [ (!0 = 0) -> (B,(\(x0 : B) -> x0,\(a : B) -> ((a,<!0> a),\(z : Sigma B (\(x0 : B) -> IdP (<!0> B) a x0)) -> <!0> (z.2 @ !0,<!1> z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ]))) -> <!1> (glueElem (comp (<!2> B) b [ (!0 = 0) -> <!2> v.2 @ (!1 /\ !2), (!0 = 1) -> <!2> ((w.2.2 b).2 v @ !1).2 @ !2, (!1 = 0) -> <!2> comp (<!3> B) b [ (!0 = 0) -> <!3> b, (!0 = 1) -> <!3> (w.2.2 b).1.2 @ (!2 /\ !3), (!2 = 0) -> <!3> b ], (!1 = 1) -> <!2> v.2 @ !2 ]) [ (!0 = 0) -> v.2 @ !1, (!0 = 1) -> ((w.2.2 b).2 v @ !1).1 ],<!2> comp (<!3> B) b [ (!0 = 0) -> <!3> v.2 @ (!1 /\ !2 /\ !3), (!0 = 1) -> <!3> ((w.2.2 b).2 v @ !1).2 @ (!2 /\ !3), (!1 = 0) -> <!3> comp (<!4> B) b [ (!0 = 0) -> <!4> b, (!0 = 1) -> <!4> (w.2.2 b).1.2 @ (!2 /\ !3 /\ !4), (!2 = 0) -> <!4> b, (!3 = 0) -> <!4> b ], (!1 = 1) -> <!3> v.2 @ (!2 /\ !3), (!2 = 0) -> <!3> b ])))))
 
 contrSingl' (A : U) (a b : A) (p : Id A a b) :
   Id ((x:A) * Id A x b) (b,refl A b) (a,p) = <i> (p @ -i,<j> p @ -i\/j)
@@ -142,52 +142,29 @@ corrUniv' (A B : U) : equiv (Id U A B) (equiv A B) =
   (transEquiv' B A,univalence B A)
 
 
--- -- Some tests of normal forms:
--- testUniv1 (A : U) : Id U A A =
---   trans (equiv A A) (Id U A A) (<i> corrUniv A A @ -i) (idEquiv A)
-
--- -- obtained by normal form
--- ntestUniv1 (A:U) : Id U A A =
---  <i> comp (<_>U)
---       (comp (<_>U) A
---          [ (i = 0) -> <l> comp (<_>U) A [ (l = 0) -> <i> glue A [ (i = 0) -> (A,(\(x : A) -> x,\(a : A) -> ((a,<l> a),\(z : ((x : A) * IdP (<l> A) a x)) -> <l> (z.2 @ l,<i> z.2 @ (l /\ i))))), (i = 1) -> (A,(comp (<l> A -> A) (\(x : A) -> x) [],comp (<l> (y : A) ->
---   ((x : ((x : A) * IdP (<j> A) y (comp (<j> A) (comp (<i> A) x []) [ (l = 0) -> <j> comp (<k> A) x [ (j = 1) -> <k> x ] ]))) *    (y0 : ((x0 : A) * IdP (<j> A) y (comp (<j> A) (comp (<i> A) x0 []) [ (l = 0) -> <j> comp (<k> A) x0 [ (j = 1) -> <k> x0 ] ]))) -> IdP (<j> ((x0 : A) * IdP (<j> A) y (comp (<j> A) (comp (<i> A) x0 []) [ (l = 0) -> <j> comp (<k> A) x0 [ (j = 1) -> <k> x0 ] ]))) x y0)) (\(a : A) -> ((a,<l> a),\(z : ((x : A) * IdP (<l> A) a x)) -> <l> (z.2 @ l,<i> z.2 @ (l /\ i)))) [])) ], (l = 1) -> <i> glue A [ (i = 0) -> (A,(\(x : A) -> x,\(a : A) -> ((a,<l> a),\(z : ((x : A) * IdP (<l> A) a x)) -> <l> (z.2 @ l,<i> z.2 @ (l /\ i))))), (i = 1) -> (A,(comp (<l> A -> A) (\(x : A) -> x) [],comp (<l> (y : A) ->
---         ((x : ((x : A) * IdP (<j> A) y (comp (<j> A) (comp (<i> A) x []) [ (l = 0) -> <j> comp (<k> A) x [ (j = 1) -> <k> x ] ]))) * (y0 : ((x0 : A) * IdP (<j> A) y (comp (<j> A) (comp (<i> A) x0 []) [ (l = 0) -> <j> comp (<k> A) x0 [ (j = 1) -> <k> x0 ] ]))) -> IdP (<j> ((x0 : A) * IdP (<j> A) y (comp (<j> A) (comp (<i> A) x0 []) [ (l = 0) -> <j> comp (<k> A) x0 [ (j = 1) -> <k> x0 ] ]))) x y0)) (\(a : A) -> ((a,<l> a),\(z : ((x : A) * IdP (<l> A) a x)) -> <l> (z.2 @ l,<i> z.2 @ (l /\ i)))) [])) ] ], (i = 1) -> <l> A ]) [ (i = 0) -> <l> A, (i = 1) -> <l> A ]
-
--- testUniv2 : bool = trans bool bool (ntestUniv1 bool) true
-
--- ntestUniv2 : bool =
---  comp (<i> comp (<_>U) (comp (<_>U) bool [ (i = 0) -> <j> comp (<_>U) bool [ (j = 0) -> <i> glue bool [ (i = 0) -> (bool,(\(x : bool) -> x,\(a : bool) -> ((a,<i> a),\(z : ((x : bool) * IdP (<i> bool) a x)) -> <i> (z.2 @ i,<j> z.2 @ (i /\ j))))), (i = 1) -> (bool,(comp (<i> bool -> bool) (\(x : bool) -> x) [],comp (<i> (y : bool) ->
---   ((x : ((x : bool) * IdP (<j> bool) y (comp (<j> bool) (comp (<i> bool) x []) [ (i = 0) -> <j> comp (<k> bool) x [ (j = 1) -> <k> x ] ]))) * (y0 : ((x0 : bool) * IdP (<j> bool) y (comp (<j> bool) (comp (<i> bool) x0 []) [ (i = 0) -> <j> comp (<k> bool) x0 [ (j = 1) -> <k> x0 ] ]))) -> IdP (<j> ((x0 : bool) * IdP (<k> bool) y (comp (<j> bool) (comp (<i> bool) x0 []) [ (i = 0) -> <j> comp (<k> bool) x0 [ (j = 1) -> <k> x0 ] ]))) x y0)) (\(a : bool) -> ((a,<i> a),\(z : ((x : bool) * IdP (<i> bool) a x)) -> <i> (z.2 @ i,<j> z.2 @ (i /\ j)))) [])) ], (j = 1) -> <i> glue bool [ (i = 0) -> (bool,(\(x : bool) -> x,\(a : bool) -> ((a,<i> a),\(z : ((x : bool) * IdP (<i> bool) a x)) -> <i> (z.2 @ i,<j> z.2 @ (i /\ j))))), (i = 1) -> (bool,(comp (<i> bool -> bool) (\(x : bool) -> x) [],comp (<i> (y : bool) ->
---   ((x : ((x : bool) * IdP (<j> bool) y (comp (<j> bool) (comp (<i> bool) x []) [ (i = 0) -> <j> comp (<k> bool) x [ (j = 1) -> <k> x ] ]))) * (y0 : ((x0 : bool) * IdP (<j> bool) y (comp (<j> bool) (comp (<i> bool) x0 []) [ (i = 0) -> <j> comp (<k> bool) x0 [ (j = 1) -> <k> x0 ] ]))) -> IdP (<j> ((x0 : bool) * IdP (<k> bool) y (comp (<j> bool) (comp (<i> bool) x0 []) [ (i = 0) -> <j> comp (<k> bool) x0 [ (j = 1) -> <k> x0 ] ]))) x y0)) (\(a : bool) -> ((a,<i> a),\(z : ((x : bool) * IdP (<i> bool) a x)) -> <i> (z.2 @ i,<j> z.2 @ (i /\ j)))) [])) ] ], (i = 1) -> <j> bool ]) [ (i = 0) -> <j> bool, (i = 1) -> <j> bool ]) true []
-
-
--- ------------------------------------------------------------------------------
--- -- The direct proof of univalence using transEquiv which is too slow
--- -- to normalize:
-
--- -- transEquiv is an equiv
--- transEquivIsEquiv (A B : U)
---   : isEquiv (Id U A B) (equiv A B) (transEquiv A B)
---   = gradLemma (Id U A B) (equiv A B) (transEquiv A B)
---       (transEquivToId A B) (idToId A B) (eqToEq A B)
-
--- -- Univalence proved using transEquiv
--- univalenceTrans (A B:U) : Id U (Id U A B) (equiv A B) = 
---  isoId (Id U A B) (equiv A B) (transEquiv A B)
---        (transEquivToId A B) (idToId A B) (eqToEq A B)
-
--- univalenceTrans' (A B : U) : equiv (Id U A B) (equiv A B) =
---   (transEquiv A B,transEquivIsEquiv A B)
-
--- -- univalenceTrans takes extremely much memory when normalizing
-
--- -- This also takes too long to normalize:
--- slowtest (A : U) : Id (equiv A A)
---   (transEquiv A A (transEquivToId A A (idEquiv A))) (idEquiv A) =
---     idToId A A (idEquiv A)
-
-
+------------------------------------------------------------------------------
+-- The direct proof of univalence using transEquiv which is too slow
+-- to normalize:
+
+-- transEquiv is an equiv
+transEquivIsEquiv (A B : U)
+  : isEquiv (Id U A B) (equiv A B) (transEquiv A B)
+  = gradLemma (Id U A B) (equiv A B) (transEquiv A B)
+      (transEquivToId A B) (idToId A B) (eqToEq A B)
+
+-- Univalence proved using transEquiv
+-- univalenceTrans takes extremely much memory when normalizing
+univalenceTrans (A B:U) : Id U (Id U A B) (equiv A B) = 
+ isoId (Id U A B) (equiv A B) (transEquiv A B)
+       (transEquivToId A B) (idToId A B) (eqToEq A B)
+
+univalenceTrans' (A B : U) : equiv (Id U A B) (equiv A B) =
+  (transEquiv A B,transEquivIsEquiv A B)
+
+-- This also takes too long to normalize:
+slowtest (A : U) : Id (equiv A A)
+  (transEquiv A A (transEquivToId A A (idEquiv A))) (idEquiv A) =
+    idToId A A (idEquiv A)
 
 
 -- ------------------------------------------------------------------------------