add IdPathTest1

diff --git a/examples/prelude.ctt b/examples/prelude.ctt
index da8bf9b775aa6ba2d735aebff31bc0d16c4df020..f4825b16371318c1b309f3f072f9c19cb86b4e96 100644 (file)
--- a/examples/prelude.ctt
+++ b/examples/prelude.ctt
@@ -107,6 +107,10 @@ lemSimpl (A : U) (a b c : A) (p : Id A a b) (q q' : Id A b c)
            , (k = 0)  -> p
            , (k = 1)  -> s @ j ]
 
+IdPathTest1 (A : U) (a b : A) (p : Id A a b) :
+  Id (Id A a b) p (<i> comp (<_> A) (p @ i) [(i=0) -> <_> a,(i=1) -> <_> b]) = 
+  <j i> fill (<_> A) (p @ i) [(i=0) -> <_> a,(i=1) -> <_> b] @ j
+
 idfun (A : U) (a : A) : A = a
 
 --         u