From: Simon Huber <hubsim@gmail.com>
Date: Tue, 24 Mar 2015 10:29:44 +0000 (+0100)
Subject: lemTest not in prelude..
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=13440b3db3eab3f8bd6e7fe5e42e775fa1f388b7;p=cubicaltt.git

lemTest not in prelude..
---

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 = <i> 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 =
       <i> 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