From: Anders Mörtberg <andersmortberg@gmail.com>
Date: Wed, 9 Dec 2015 19:15:03 +0000 (-0500)
Subject: add IdPathTest1
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=9b2c36453f6ef6527f84008a6843a1d2d1cf3de5;p=cubicaltt.git

add IdPathTest1
---

diff --git a/examples/prelude.ctt b/examples/prelude.ctt
index da8bf9b..f4825b1 100644
--- 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