From: coquand <coquand@chalmers.se>
Date: Thu, 30 Apr 2015 11:56:57 +0000 (+0200)
Subject: added some test for pi1S2
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=16bb6f312a06e811d403b21a70f841c1c038f8e7;p=cubicaltt.git

added some test for pi1S2
---

diff --git a/examples/pi1S2.ctt b/examples/pi1S2.ctt
index 308de0b..561f9e3 100644
--- a/examples/pi1S2.ctt
+++ b/examples/pi1S2.ctt
@@ -32,4 +32,13 @@ pi1stwo : U = sTrunc (Id stwo north north)
 
 eqPi1 : Id U pi1S2 pi1stwo = <i>sTrunc (Id (susp (eqS1@i)) north north)
 
-propPi1stwo : prop pi1stwo = subst U prop pi1S2 pi1stwo eqPi1 propPi1S2
\ No newline at end of file
+propPi1stwo : prop pi1stwo = subst U prop pi1S2 pi1stwo eqPi1 propPi1S2
+
+meridNstwo : Id stwo north south = <i>merid{stwo} north@i
+meridSstwo : Id stwo north south = <i>merid{stwo} south@i
+trivstwo : pi1stwo = inc (refl stwo north)
+loopstwo : pi1stwo = inc (compId stwo north south north meridNstwo (<i>meridSstwo@-i))
+
+
+test2 : Id pi1stwo trivstwo loopstwo = propPi1stwo trivstwo loopstwo
+test3 : Id pi1stwo trivstwo trivstwo = propPi1stwo trivstwo trivstwo