From dfbefc6282efb96cf3ec0a51ff91c03ee893483c Mon Sep 17 00:00:00 2001 From: coquand Date: Sat, 26 Dec 2015 13:26:42 +0100 Subject: [PATCH] updated testContr --- examples/testContr.ctt | 13 +++++++++++++ 1 file changed, 13 insertions(+) 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) -- 2.34.1