From: Anders Mörtberg Date: Thu, 14 Jan 2016 15:36:33 +0000 (-0500) Subject: add nlem1 X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=779b4c51ecff533888c032d153c5f1891013649f;p=cubicaltt.git add nlem1 --- diff --git a/examples/univalence.ctt b/examples/univalence.ctt index 28b7658..697a388 100644 --- a/examples/univalence.ctt +++ b/examples/univalence.ctt @@ -77,9 +77,8 @@ 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 --- equivFunFib (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) = --- \ (z:C x) -> ((comp ( B (comp ( A) cC.1.1 [ (i = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ j).1, (i = 1) -> (cC.2 ((x,z)) @ j).1 ])) cB.1.2 [], comp ( C (comp ( A) cC.1.1 [ (i = 0) -> (cC.2 ((x,z)) @ k).1, (i = 1)(j = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ k).1, (j = 1) -> (cC.2 ((x,z)) @ k).1 ])) (comp ( C (comp ( A) cC.1.1 [ (i = 0) -> (cC.2 ((x,z)) @ (j /\ k)).1, (i = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ k)).1, (j = 0) -> cC.1.1 ])) cC.1.2 [ (i = 0) -> (cC.2 ((x,z)) @ j).2, (i = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ j).2 ]) [ (i = 0) -> z, (i = 1) -> f (comp ( A) cC.1.1 [ (j = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ k).1, (j = 1) -> (cC.2 ((x,z)) @ k).1 ]) (comp ( B (comp ( A) cC.1.1 [ (j = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1, (j = 1)(k = 1) -> (cC.2 ((x,z)) @ i).1, (k = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1 ])) cB.1.2 [ (j = 0) -> cB.1.2 ]) ]),\(x0 : Sigma (B x) (\(x0 : B x) -> IdP ( C x) z (f x x0))) -> (comp ( B x) (comp ( B (comp ( A) cC.1.1 [ (i = 0) -> comp ( A) cC.1.1 [ (j = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (k /\ l)).1, (j = 1) -> (cC.2 ((x,z)) @ (k /\ l)).1, (k = 0) -> cC.1.1 ], (i = 1) -> (cC.2 ((x,x0.2 @ -j)) @ k).1, (j = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ k).1, (j = 1) -> (cC.2 ((x,z)) @ k).1 ])) (cB.2 ((x,x0.1)) @ i).2 []) [ (i = 0) -> comp ( B (comp ( A) cC.1.1 [ (i = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ k).1, (i = 1) -> (cC.2 ((x,z)) @ k).1 ])) cB.1.2 [], (i = 1) -> comp ( B x) x0.1 [ (j = 1) -> x0.1 ] ], comp ( C x) (comp ( C (comp ( A) cC.1.1 [ (i = 0) -> comp ( A) cC.1.1 [ (j = 0) -> cC.1.1, (k = 0) -> (cC.2 ((x,z)) @ (j /\ m)).1, (k = 1)(l = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ m)).1, (l = 1) -> (cC.2 ((x,z)) @ (j /\ m)).1 ], (i = 1) -> (cC.2 ((x,x0.2 @ (-l /\ k))) @ j).1, (k = 0) -> (cC.2 ((x,z)) @ j).1, (k = 1)(l = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ j).1, (l = 1) -> (cC.2 ((x,z)) @ j).1 ])) (comp ( C (comp ( A) cC.1.1 [ (i = 0) -> comp ( A) cC.1.1 [ (j = 0) -> cC.1.1, (k = 0) -> (cC.2 ((x,z)) @ (l /\ j /\ m)).1, (k = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (l /\ j /\ m)).1, (l = 0) -> cC.1.1 ], (i = 1) -> (cC.2 ((x,x0.2 @ k)) @ (l /\ j)).1, (k = 0) -> (cC.2 ((x,z)) @ (l /\ j)).1, (k = 1) -> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ (l /\ j)).1, (l = 0) -> cC.1.1 ])) cC.1.2 [ (i = 0) -> comp ( C (comp ( A) cC.1.1 [ (j = 0) -> cC.1.1, (k = 0) -> (cC.2 ((x,z)) @ (l /\ j /\ m)).1, (k = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (l /\ j /\ m)).1, (l = 0) -> cC.1.1 ])) cC.1.2 [ (k = 0) -> (cC.2 ((x,z)) @ (l /\ j)).2, (k = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (l /\ j)).2, (l = 0) -> cC.1.2 ], (i = 1) -> (cC.2 ((x,x0.2 @ k)) @ l).2, (k = 0) -> (cC.2 ((x,z)) @ l).2, (k = 1) -> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ l).2 ]) [ (k = 0) -> z, (k = 1) -> f (comp ( A) cC.1.1 [ (i = 0) -> comp ( A) cC.1.1 [ (k = 0) -> cC.1.1, (l = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (k /\ j)).1, (l = 1) -> (cC.2 ((x,z)) @ (k /\ j)).1 ], (i = 1) -> (cC.2 ((x,x0.2 @ -l)) @ k).1, (l = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ k).1, (l = 1) -> (cC.2 ((x,z)) @ k).1 ]) (comp ( B (comp ( A) cC.1.1 [ (i = 0) -> comp ( A) cC.1.1 [ (j = 0) -> cC.1.1, (k = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ m)).1, (k = 1)(l = 1) -> (cC.2 ((x,z)) @ (j /\ m)).1, (l = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ m)).1 ], (i = 1) -> (cC.2 ((x,x0.2 @ (-l \/ -k))) @ j).1, (k = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ j).1, (k = 1)(l = 1) -> (cC.2 ((x,z)) @ j).1, (l = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ j).1 ])) (cB.2 ((x,x0.1)) @ i).2 [ (l = 0) -> (cB.2 ((x,x0.1)) @ i).2 ]) ]) [ (i = 0) -> comp ( C (comp ( A) cC.1.1 [ (j = 0)(k = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1, (j = 1) -> (cC.2 ((x,z)) @ i).1, (k = 0) -> (cC.2 ((x,z)) @ i).1 ])) (comp ( C (comp ( A) cC.1.1 [ (j = 0) -> cC.1.1, (k = 0) -> (cC.2 ((x,z)) @ (j /\ i)).1, (k = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ i)).1 ])) cC.1.2 [ (k = 0) -> (cC.2 ((x,z)) @ j).2, (k = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ j).2 ]) [ (k = 0) -> z, (k = 1) -> f (comp ( A) cC.1.1 [ (j = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ l).1, (j = 1) -> (cC.2 ((x,z)) @ l).1 ]) (comp ( B (comp ( A) cC.1.1 [ (j = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1, (j = 1)(l = 1) -> (cC.2 ((x,z)) @ i).1, (l = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1 ])) cB.1.2 [ (j = 0) -> cB.1.2 ]) ], (i = 1) -> comp ( C x) (x0.2 @ k) [ (k = 0) -> z, (k = 1) -> f x (comp ( B x) x0.1 [ (j = 0) -> x0.1, (l = 1) -> x0.1 ]), (l = 1) -> x0.2 @ k ], (k = 0) -> z, (k = 1) -> f x (comp ( B x) (comp ( B (comp ( A) cC.1.1 [ (i = 0) -> comp ( A) cC.1.1 [ (k = 0) -> cC.1.1, (l = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (k /\ j)).1, (l = 1) -> (cC.2 ((x,z)) @ (k /\ j)).1 ], (i = 1) -> (cC.2 ((x,x0.2 @ -l)) @ k).1, (l = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ k).1, (l = 1) -> (cC.2 ((x,z)) @ k).1 ])) (cB.2 ((x,x0.1)) @ i).2 []) [ (i = 0) -> comp ( B (comp ( A) cC.1.1 [ (i = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ k).1, (i = 1) -> (cC.2 ((x,z)) @ k).1 ])) cB.1.2 [], (i = 1) -> comp ( B x) x0.1 [ (k = 1)(l = 1) -> x0.1 ], (l = 0) -> comp ( B (comp ( A) cC.1.1 [ (i = 0) -> comp ( A) cC.1.1 [ (k = 0) -> cC.1.1, (l = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (k /\ j)).1, (l = 1) -> (cC.2 ((x,z)) @ (k /\ j)).1 ], (i = 1) -> (cC.2 ((x,x0.2 @ -l)) @ k).1, (l = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ k).1, (l = 1) -> (cC.2 ((x,z)) @ k).1 ])) (cB.2 ((x,x0.1)) @ i).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 ( 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 ( Sigma A (\(x0 : A) -> C x0)) x y)) -> \(x : A) -> \(z : C x) -> ((comp ( B (comp ( A) cC.1.1 [ (!0 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !1).1, (!0 = 1) -> (cC.2 ((x,z)) @ !1).1 ])) cB.1.2 [], comp ( C (comp ( A) cC.1.1 [ (!0 = 0) -> (cC.2 ((x,z)) @ !2).1, (!0 = 1)(!1 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !2).1, (!1 = 1) -> (cC.2 ((x,z)) @ !2).1 ])) (comp ( C (comp ( A) cC.1.1 [ (!0 = 0) -> (cC.2 ((x,z)) @ (!1 /\ !2)).1, (!0 = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!1 /\ !2)).1, (!1 = 0) -> cC.1.1 ])) cC.1.2 [ (!0 = 0) -> (cC.2 ((x,z)) @ !1).2, (!0 = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !1).2 ]) [ (!0 = 0) -> z, (!0 = 1) -> f (comp ( A) cC.1.1 [ (!1 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !2).1, (!1 = 1) -> (cC.2 ((x,z)) @ !2).1 ]) (comp ( B (comp ( A) cC.1.1 [ (!1 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !3).1, (!1 = 1)(!2 = 1) -> (cC.2 ((x,z)) @ !3).1, (!2 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !3).1 ])) cB.1.2 [ (!1 = 0) -> cB.1.2 ]) ]),\(x0 : Sigma (B x) (\(x0 : B x) -> IdP ( C x) z (f x x0))) -> (comp ( B x) (comp ( B (comp ( A) cC.1.1 [ (!0 = 0) -> comp ( A) cC.1.1 [ (!1 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!2 /\ !3)).1, (!1 = 1) -> (cC.2 ((x,z)) @ (!2 /\ !3)).1, (!2 = 0) -> cC.1.1 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ -!1)) @ !2).1, (!1 = 0) -> (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) -> (cC.2 ((x,z)) @ !2).1 ])) (cB.2 ((x,x0.1)) @ !0).2 []) [ (!0 = 0) -> comp ( B (comp ( A) cC.1.1 [ (!0 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !1).1, (!0 = 1) -> (cC.2 ((x,z)) @ !1).1 ])) cB.1.2 [], (!0 = 1) -> comp ( B x) x0.1 [ (!1 = 1) -> x0.1 ] ], comp ( C x) (comp ( C (comp ( A) cC.1.1 [ (!0 = 0) -> comp ( A) cC.1.1 [ (!2 = 0) -> (cC.2 ((x,z)) @ (!4 /\ !5)).1, (!2 = 1)(!3 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!4 /\ !5)).1, (!3 = 1) -> (cC.2 ((x,z)) @ (!4 /\ !5)).1, (!4 = 0) -> cC.1.1 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ (!2 /\ -!3))) @ !4).1, (!2 = 0) -> (cC.2 ((x,z)) @ !4).1, (!2 = 1)(!3 = 0) -> (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) -> (cC.2 ((x,z)) @ !4).1 ])) (comp ( C (comp ( A) cC.1.1 [ (!0 = 0) -> comp ( A) cC.1.1 [ (!2 = 0) -> (cC.2 ((x,z)) @ (!3 /\ !4 /\ !5)).1, (!2 = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!3 /\ !4 /\ !5)).1, (!3 = 0) -> cC.1.1, (!4 = 0) -> cC.1.1 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ !2)) @ (!3 /\ !4)).1, (!2 = 0) -> (cC.2 ((x,z)) @ (!3 /\ !4)).1, (!2 = 1) -> (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) -> cC.1.1 ])) cC.1.2 [ (!0 = 0) -> comp ( C (comp ( A) cC.1.1 [ (!2 = 0) -> (cC.2 ((x,z)) @ (!3 /\ !4 /\ !5)).1, (!2 = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!3 /\ !4 /\ !5)).1, (!3 = 0) -> cC.1.1, (!4 = 0) -> cC.1.1 ])) cC.1.2 [ (!2 = 0) -> (cC.2 ((x,z)) @ (!3 /\ !4)).2, (!2 = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!3 /\ !4)).2, (!3 = 0) -> cC.1.2 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ !2)) @ !3).2, (!2 = 0) -> (cC.2 ((x,z)) @ !3).2, (!2 = 1) -> (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) -> z, (!2 = 1) -> f (comp ( A) cC.1.1 [ (!0 = 0) -> comp ( A) cC.1.1 [ (!3 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!4 /\ !5)).1, (!3 = 1) -> (cC.2 ((x,z)) @ (!4 /\ !5)).1, (!4 = 0) -> cC.1.1 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ -!3)) @ !4).1, (!3 = 0) -> (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) -> (cC.2 ((x,z)) @ !4).1 ]) (comp ( B (comp ( A) cC.1.1 [ (!0 = 0) -> comp ( A) cC.1.1 [ (!3 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!5 /\ !6)).1, (!3 = 1)(!4 = 1) -> (cC.2 ((x,z)) @ (!5 /\ !6)).1, (!4 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!5 /\ !6)).1, (!5 = 0) -> cC.1.1 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ (-!3 \/ -!4))) @ !5).1, (!3 = 0) -> (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) -> (cC.2 ((x,z)) @ !5).1, (!4 = 0) -> (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) -> (cB.2 ((x,x0.1)) @ !0).2 ]) ]) [ (!0 = 0) -> comp ( C (comp ( A) cC.1.1 [ (!2 = 0) -> (cC.2 ((x,z)) @ !4).1, (!2 = 1)(!3 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !4).1, (!3 = 1) -> (cC.2 ((x,z)) @ !4).1 ])) (comp ( C (comp ( A) cC.1.1 [ (!2 = 0) -> (cC.2 ((x,z)) @ (!3 /\ !4)).1, (!2 = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!3 /\ !4)).1, (!3 = 0) -> cC.1.1 ])) cC.1.2 [ (!2 = 0) -> (cC.2 ((x,z)) @ !3).2, (!2 = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !3).2 ]) [ (!2 = 0) -> z, (!2 = 1) -> f (comp ( A) cC.1.1 [ (!3 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !4).1, (!3 = 1) -> (cC.2 ((x,z)) @ !4).1 ]) (comp ( B (comp ( A) cC.1.1 [ (!3 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !5).1, (!3 = 1)(!4 = 1) -> (cC.2 ((x,z)) @ !5).1, (!4 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !5).1 ])) cB.1.2 [ (!3 = 0) -> cB.1.2 ]) ], (!0 = 1) -> comp ( C x) (x0.2 @ !2) [ (!2 = 0) -> z, (!2 = 1) -> f x (comp ( B x) x0.1 [ (!3 = 1) -> x0.1, (!4 = 0) -> x0.1 ]), (!3 = 1) -> x0.2 @ !2 ], (!2 = 0) -> z, (!2 = 1) -> f x (comp ( B x) (comp ( B (comp ( A) cC.1.1 [ (!0 = 0) -> comp ( A) cC.1.1 [ (!1 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!2 /\ !3)).1, (!1 = 1) -> (cC.2 ((x,z)) @ (!2 /\ !3)).1, (!2 = 0) -> cC.1.1 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ -!1)) @ !2).1, (!1 = 0) -> (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) -> (cC.2 ((x,z)) @ !2).1 ])) (cB.2 ((x,x0.1)) @ !0).2 []) [ (!0 = 0) -> comp ( B (comp ( A) cC.1.1 [ (!0 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !1).1, (!0 = 1) -> (cC.2 ((x,z)) @ !1).1 ])) cB.1.2 [], (!0 = 1) -> comp ( B x) x0.1 [ (!3 = 1)(!4 = 1) -> x0.1 ], (!3 = 0) -> comp ( B (comp ( A) cC.1.1 [ (!0 = 0) -> comp ( A) cC.1.1 [ (!1 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!2 /\ !3)).1, (!1 = 1) -> (cC.2 ((x,z)) @ (!2 /\ !3)).1, (!2 = 0) -> cC.1.1 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ -!1)) @ !2).1, (!1 = 0) -> (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) -> (cC.2 ((x,z)) @ !2).1 ])) (cB.2 ((x,x0.1)) @ !0).2 [] ]) ])) + lem1 (B:U) : isContr ((X:U) * equiv X B) = ((B,idEquiv B) @@ -115,6 +114,8 @@ 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, a),\(z : Sigma B (\(x : B) -> IdP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))),\(w : Sigma U (\(X : U) -> Sigma (X -> B) (\(f : X -> B) -> (y : B) -> Sigma (Sigma X (\(x : X) -> IdP ( B) y (f x))) (\(x : Sigma X (\(x : X) -> IdP ( B) y (f x))) -> (y0 : Sigma X (\(x0 : X) -> IdP ( B) y (f x0))) -> IdP ( Sigma X (\(x0 : X) -> IdP ( B) y (f x0))) x y0)))) -> (glue B [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> IdP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ],(\(g : glue B [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> IdP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ]) -> unglueElem g [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> IdP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ],\(b : B) -> ((glueElem (comp ( B) b [ (!0 = 0) -> b, (!0 = 1) -> (w.2.2 b).1.2 @ !1 ]) [ (!0 = 0) -> b, (!0 = 1) -> (w.2.2 b).1.1 ], comp ( B) b [ (!0 = 0) -> b, (!0 = 1) -> (w.2.2 b).1.2 @ (!1 /\ !2), (!1 = 0) -> b ]),\(v : Sigma (glue B [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> IdP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ]) (\(x : glue B [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> IdP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ]) -> IdP ( B) b (unglueElem x [ (!0 = 0) -> (B,(\(x0 : B) -> x0,\(a : B) -> ((a, a),\(z : Sigma B (\(x0 : B) -> IdP ( B) a x0)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ]))) -> (glueElem (comp ( B) b [ (!0 = 0) -> v.2 @ (!1 /\ !2), (!0 = 1) -> ((w.2.2 b).2 v @ !1).2 @ !2, (!1 = 0) -> comp ( B) b [ (!0 = 0) -> b, (!0 = 1) -> (w.2.2 b).1.2 @ (!2 /\ !3), (!2 = 0) -> b ], (!1 = 1) -> v.2 @ !2 ]) [ (!0 = 0) -> v.2 @ !1, (!0 = 1) -> ((w.2.2 b).2 v @ !1).1 ], comp ( B) b [ (!0 = 0) -> v.2 @ (!1 /\ !2 /\ !3), (!0 = 1) -> ((w.2.2 b).2 v @ !1).2 @ (!2 /\ !3), (!1 = 0) -> comp ( B) b [ (!0 = 0) -> b, (!0 = 1) -> (w.2.2 b).1.2 @ (!2 /\ !3 /\ !4), (!2 = 0) -> b, (!3 = 0) -> b ], (!1 = 1) -> v.2 @ (!2 /\ !3), (!2 = 0) -> 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) = (p @ -i, p @ -i\/j)