remove duplicate code

diff --git a/examples/collection.ctt b/examples/collection.ctt
index d68f71053d442a83a29073c19929df7e85947561..bb751dd6e037f76ab31b44963603236a9c4e65d9 100644 (file)
--- a/examples/collection.ctt
+++ b/examples/collection.ctt
@@ -1,53 +1,35 @@
+-- This file proves that the collection of all sets is a groupoid
 module collection where
 
-import prelude
-import equiv
 import univalence
 import sigma
 import pi
--- import testContr
 
-propIsContr (A:U) (z0 z1 : isContr A) : Id (isContr A) z0 z1 =
- <j>(p0 a1@j,
-     \ (x:A) -> 
-        <i>comp (<_>A) (lem1 x@i@j) [ (i=0) -> <k>p0 a1@j, (i=1) -> <k>p0 x@(j\/k),
-                                      (j=0) -> <k>p0 x@(i/\k), (j=1) -> <k>p1 x@i ])
- where
-  a0 : A = z0.1
-  p0 : (x:A) -> Id A a0 x = z0.2
-  a1 : A = z1.1
-  p1 : (x:A) -> Id A a1 x = z1.2
-  lem1 (x:A) : IdP (<i>Id A a0 (p1 x@i)) (p0 a1) (p0 x) = <i j> p0 (p1 x@i) @ j
- 
-propIsEquiv (A B : U) (f : A -> B)
-  : prop (isEquiv A B f) = \ (u0 u1:isEquiv A B f) -> <i> \ (y:B) -> propIsContr (fiber A B f y) (u0 y) (u1 y) @ i
+setFun (A B : U) (sB : set B) : set (A -> B) =
+ setPi A (\(x : A) -> B) (\(x : A) -> sB)
 
-setFun (A B:U) (sB: set B) : set (A -> B) = setPi A (\ (x:A) -> B) (\ (x:A) -> sB)
+eqEquivFst (A B : U) : (t u : equiv A B) ->
+     Id U (Id (equiv A B) t u) (Id (A -> B) t.1 u.1)
+   = lemSigProp (A -> B) (isEquiv A B) (propIsEquiv A B)
 
-groupoidFun (A B : U) (gB:groupoid B) : groupoid (A -> B) = groupoidPi A (\ (x:A) -> B) (\ (x:A) -> gB)
+-- groupoidFun (A B : U) (gB:groupoid B) : groupoid (A -> B) =
+--   groupoidPi A (\(x : A) -> B) (\(x : A) -> gB)
 
-lem3 (A B : U) (t u : equiv A B) : Id U (Id (equiv A B) t u) (Id (A -> B) t.1 u.1)
- = lemSigProp (A->B) (isEquiv A B) (propIsEquiv A B) t u 
+-- lem5 (A B : U) (gB:groupoid B) (t u:equiv A B) : set (Id (equiv A B) t u)
+--  = substInv U set  (Id (equiv A B) t u) (Id (A -> B) t.1 u.1)
+--             (eqEquivFst A B t u) (groupoidFun A B gB t.1 u.1)
 
-lem4 (A B : U) (sB:set B) (t u:equiv A B) : prop (Id  (equiv A B) t u)
- = substInv U prop (Id (equiv A B) t u) (Id (A -> B) t.1 u.1) (lem3 A B t u) (setFun A B sB t.1 u.1)
-
-lem5 (A B : U) (gB:groupoid B) (t u:equiv A B) : set (Id (equiv A B) t u)
- = substInv U set  (Id (equiv A B) t u) (Id (A -> B) t.1 u.1) (lem3 A B t u) (groupoidFun A B gB t.1 u.1)
-
-lem6 (A B : U) (sB : set B) : set (Id U A B) = 
- substInv U set (Id U A B)  (equiv A B) (corrUniv A B   ) (lem4 A B sB)
-
--- the collection of all sets
-
-SET : U = (X:U) * set X
+setId (A B : U) (sB : set B) : set (Id U A B) = 
+ substInv U set (Id U A B) (equiv A B) (corrUniv A B) (rem A B sB)
+  where
+  rem (A B : U) (sB:set B) (t u:equiv A B) : prop (Id (equiv A B) t u)
+    = substInv U prop (Id (equiv A B) t u) (Id (A -> B) t.1 u.1)
+            (eqEquivFst A B t u) (setFun A B sB t.1 u.1)
 
 -- the collection of all sets is a groupoid
-
-groupoidSET (A B : SET) : set (Id SET A B) = 
- rem2
- where
-   rem : set (Id U A.1 B.1) = lem6 A.1 B.1 B.2
-   rem1 : Id U (Id SET A B) (Id U A.1 B.1) = lemSigProp U set setIsProp A B
-   rem2 : set (Id SET A B) = substInv U set (Id SET A B) (Id U A.1 B.1) rem1 rem
+groupoidSET : groupoid SET = \(A B : SET) ->
+  let rem : set (Id U A.1 B.1) = setId A.1 B.1 B.2
+      rem1 : Id U (Id SET A B) (Id U A.1 B.1) =
+        lemSigProp U set setIsProp A B
+  in substInv U set (Id SET A B) (Id U A.1 B.1) rem1 rem
 

diff --git a/examples/equiv.ctt b/examples/equiv.ctt
index d8c110576c12dcb099a27c72b4d45d8880e55bf4..d8280fe484d6e95095ee174296412c4aeaf0035e 100644 (file)
--- a/examples/equiv.ctt
+++ b/examples/equiv.ctt
@@ -13,7 +13,8 @@ equiv (A B : U) : U = (f : A -> B) * isEquiv A B f
 
 propIsEquiv (A B : U) (f : A -> B)
   : prop (isEquiv A B f) = 
-  \ (u0 u1:isEquiv A B f) -> <i> \ (y:B) -> propIsContr (fiber A B f y) (u0 y) (u1 y) @ i
+  \ (u0 u1:isEquiv A B f) ->
+     <i> \ (y:B) -> propIsContr (fiber A B f y) (u0 y) (u1 y) @ i
 
 equivLemma (A B : U)
   : (v w : equiv A B) -> Id (A -> B) v.1 w.1 -> Id (equiv A B) v w

diff --git a/examples/prelude.ctt b/examples/prelude.ctt
index 4ead1a8c1ea61fd72f7d14f0a2ffec44050e05bf..dd1fc1be06fc050964b358a822e70ffc3a0535f7 100644 (file)
--- a/examples/prelude.ctt
+++ b/examples/prelude.ctt
@@ -136,6 +136,9 @@ prop (A : U) : U = (a b : A) -> Id A a b
 set (A : U) : U = (a b : A) -> prop (Id A a b)
 groupoid (A : U) : U = (a b : A) -> set (Id A a b)
 
+-- the collection of all sets
+SET : U = (X:U) * set X
+
 propSet (A : U) (h : prop A) : set A =
  \(a b : A) (p q : Id A a b) ->
    <j i> comp (<k>A) a [ (i=0) -> h a a

diff --git a/examples/sigma.ctt b/examples/sigma.ctt
index 42777846632a7ac4888d3bc9a3781d9e43f8cb74..51f15349736b8d537dfc871c82df314502fb0d10 100644 (file)
--- a/examples/sigma.ctt
+++ b/examples/sigma.ctt
@@ -3,8 +3,6 @@ module sigma where
 import prelude
 import equiv
 
--- application of this fact
-
 lemIdSig (A:U) (B : A -> U) (t u : Sigma A B) :
  Id U (Id (Sigma A B) t u) ((p : Id A t.1 u.1) * IdP (<i> B (p @ i)) t.2 u.2) =
   isoId T0 T1 f g s t where
@@ -18,15 +16,6 @@ lemIdSig (A:U) (B : A -> U) (t u : Sigma A B) :
 lemIdAnd (A B : U) (t u : and A B) :
   Id U (Id (and A B) t u) (and (Id A t.1 u.1) (Id B t.2 u.2)) = lemIdSig A (\(_ : A) -> B) t u
 
-lem (A:U) (P:A->U) (pP:(x:A) -> prop (P x)) (u v:(x:A) * P x) (p:Id A u.1 v.1) :
- Id ((x:A)*P x) u v = <i>(p@i,(lemPropF A P pP u.1 v.1 p u.2 v.2)@i)
-
-propSig (A:U) (B:A-> U) (pA:prop A) (pB : (x:A) -> prop (B x)) (t u : Sigma A B) : Id (Sigma A B) t u
- = lem A B pB t u (pA t.1 u.1)
-
-propAnd (A:U) (B:U) (pA:prop A) (pB:prop B) : prop (and A B)
-  = propSig A (\(_:A)->B) pA (\(_:A)->pB)
-
 lemTransp (A:U) (a:A) : Id A a (transport (<_>A) a) = fill (<_>A) a []
 
 funDepTr (A:U) (P:A->U) (a0 a1 :A) (p:Id A a0 a1) (u0:P a0) (u1:P a1) :

diff --git a/examples/univalence.ctt b/examples/univalence.ctt
index 95d71e06213a15b8cd78768011940d5ca2b73b3c..97cf7f2a872e9313057de5e3d51cb57045fa106f 100644 (file)
--- a/examples/univalence.ctt
+++ b/examples/univalence.ctt
@@ -78,7 +78,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) =
@@ -115,7 +115,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)