updated testContr

diff --git a/examples/testContr.ctt b/examples/testContr.ctt
index dbef95700f7111d67053e09590e78aba85e1db39..eda4f1cc25cc5c4c17ed2e37e43e746f83a2ba62 100644 (file)
--- a/examples/testContr.ctt
+++ b/examples/testContr.ctt
@@ -76,3 +76,16 @@ equivFunFib (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (cB : isContr (sig A B)
                          (funFib2 A B C f x z)
                          (retFunFib A B C f x z)
                          (isEquivContr (sig A B) (sig A C) cB cC (totalFun A B C f) (x,z))
+
+
+lemSinglContr (A:U) (a:A) : isContr ((x:A) * Id A a x) =
+ ((a,refl A a),\ (z:(x:A) * Id A a x) -> contrSingl A a z.1 z.2)
+
+lem1 (A:U) : isContr ((X:U) * equiv A X) = undefined
+
+thmUniv (t : (A X:U) -> Id U A X -> equiv A X) (A:U) : (X:U) -> isEquiv (Id U A X) (equiv A X) (t A X) =
+ equivFunFib U (\ (X:U) -> Id U A X) (equiv A) (t A) (lemSinglContr U A) (lem1 A)
+
+thmUniv (lem1 : (A:U) -> isContr ((X:U) * equiv A X)) (t : (A X:U) -> Id U A X -> equiv A X) (A:U) 
+ : (X:U) -> isEquiv (Id U A X) (equiv A X) (t A X) =
+ equivFunFib U (\ (X:U) -> Id U A X) (equiv A) (t A) (lemSinglContr U A) (lem1 A)