Add J

diff --git a/examples/nat.ctt b/examples/nat.ctt
index 5c36a483dd3191b95a177adfff4934d0bff6604c..dd64abc4a1c2b337e2a30bd77a2c92eae3bfbad3 100644 (file)
--- a/examples/nat.ctt
+++ b/examples/nat.ctt
@@ -6,7 +6,6 @@ zero' : nat = zero
 one : nat = suc zero
 two : nat = suc one
 
-
 pred : nat -> nat = split
   zero -> zero
   suc n -> n
@@ -33,7 +32,6 @@ reverse (A : U) : list A -> list A = split
   nil -> nil
   cons x xs -> append A (reverse A xs) (cons x nil)
 
-
 Id (A : U) (a0 a1 : A) : U = IdP (<?0> A) a0 a1
 
 refl (A : U) (a : A) : Id A a a = <?0> a
@@ -65,3 +63,11 @@ singl (A : U) (a : A) : U = (x : A) * Id A a x
 
 contrSingl (A : U) (a b : A) (p : Id A a b) :
   Id (singl A a) (a,refl A a) (b,p) = <?0> (p @ ?0,<?1> p @ ?0 & ?1)
+
+J (A : U) (a : A) (C : (x : A) -> Id A a x -> U)
+  (d : C a (refl A a)) (x : A) (p : Id A a x) : C x p =
+    subst (singl A a) T (a, refl A a) (x, p) (contrSingl A a x p) d
+      where T (z : singl A a) : U = C (z.1) (z.2)
+
+defEqJ (A : U) (a : A) (C : (x : A) -> Id A a x -> U) (d : C a (refl A a)) :
+       Id (C a (refl A a)) (J A a C d a (refl A a)) d = refl (C a (refl A a)) d