From 16bb6f312a06e811d403b21a70f841c1c038f8e7 Mon Sep 17 00:00:00 2001
From: coquand <coquand@chalmers.se>
Date: Thu, 30 Apr 2015 13:56:57 +0200
Subject: [PATCH] added some test for pi1S2

---
 examples/pi1S2.ctt | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

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