From 13440b3db3eab3f8bd6e7fe5e42e775fa1f388b7 Mon Sep 17 00:00:00 2001 From: Simon Huber Date: Tue, 24 Mar 2015 11:29:44 +0100 Subject: [PATCH] lemTest not in prelude.. --- examples/bool.ctt | 5 +++++ examples/prelude.ctt | 4 ---- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/examples/bool.ctt b/examples/bool.ctt index 71520f1..8e24510 100644 --- a/examples/bool.ctt +++ b/examples/bool.ctt @@ -41,6 +41,11 @@ boolEqF2 : Id U bool F2 = negF2 : F2 -> F2 = subst U (\(X : U) -> (X -> X)) bool F2 boolEqF2 neg + +lemTest (A : U) : (B : U) (p : Id U A B) (a : A) -> IdP p a (transport p a) = + J U A (\(B : U) (p : Id U A B) -> (a : A) -> IdP p a (transport p a)) (refl A) + + test : IdP boolEqF2 true one = glueElem one [ (i = 0) -> true ] test1 : IdP boolEqF2 true one = lemTest bool F2 boolEqF2 true diff --git a/examples/prelude.ctt b/examples/prelude.ctt index b0fee3c..cb0f4b6 100644 --- a/examples/prelude.ctt +++ b/examples/prelude.ctt @@ -37,7 +37,3 @@ isoId (A B : U) (f : A -> B) (g : B -> A) (s : (y:B) -> Id B (f (g y)) y) (t : (x:A) -> Id A (g (f x)) x) : Id U A B = glue B [ (i = 0) -> (A,(f,(g,(s,t)))) ] - -lemTest (A : U) : (B : U) (p : Id U A B) (a : A) -> IdP p a (transport p a) = - J U A (\(B : U) (p : Id U A B) -> (a : A) -> IdP p a (transport p a)) rem - where rem (a : A) : Id A a a = refl A a \ No newline at end of file -- 2.34.1