From c9313866391efc99d2f8db5998753511bd734b32 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Wed, 27 Jan 2016 15:35:27 -0500 Subject: [PATCH] add a small test of the grad lemma --- examples/equiv.ctt | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/examples/equiv.ctt b/examples/equiv.ctt index 4b24fa7..d8c1105 100644 --- a/examples/equiv.ctt +++ b/examples/equiv.ctt @@ -58,7 +58,7 @@ transEquiv (A B:U) (p:Id U A B) : equiv A B = (f,p) 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) -idEquiv (A:U) : equiv A A = (\ (x:A) -> x, lemSinglContr A) +idEquiv (A:U) : equiv A A = (\ (x:A) -> x, lemSinglContr A) transEquiv (A X:U) (p:Id U A X) : equiv A X = substTrans U (equiv A) A X p (idEquiv A) @@ -158,3 +158,7 @@ isoId (A B : U) (f : A -> B) (g : B -> A) (t : (x : A) -> Id A (g (f x)) x) : Id U A B = glue B [ (i = 0) -> (A,f,gradLemma A B f g s t) , (i = 1) -> (B,idfun B,idIsEquiv B) ] + +idIsEquivGrad (A : U) : isEquiv A A (idfun A) = + gradLemma A A (idfun A) (idfun A) (\(a : A) -> a) (\(a : A) -> a) + -- 2.34.1