From: coquand <coquand@chalmers.se>
Date: Sat, 26 Dec 2015 12:26:42 +0000 (+0100)
Subject: updated testContr
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=dfbefc6282efb96cf3ec0a51ff91c03ee893483c;p=cubicaltt.git

updated testContr
---

diff --git a/examples/testContr.ctt b/examples/testContr.ctt
index dbef957..eda4f1c 100644
--- 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)