From 9b2c36453f6ef6527f84008a6843a1d2d1cf3de5 Mon Sep 17 00:00:00 2001
From: =?utf8?q?Anders=20M=C3=B6rtberg?= <andersmortberg@gmail.com>
Date: Wed, 9 Dec 2015 14:15:03 -0500
Subject: [PATCH] add IdPathTest1

---
 examples/prelude.ctt | 4 ++++
 1 file changed, 4 insertions(+)

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
-- 
2.34.1