From: Anders Mörtberg <mortberg@chalmers.se>
Date: Tue, 5 May 2015 00:43:47 +0000 (+0200)
Subject: Swap test2 and test3 to correspond to what is in cubical
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=357a082a18bf1923d7b810349a36379fb18972a4;p=cubicaltt.git

Swap test2 and test3 to correspond to what is in cubical
---

diff --git a/examples/pi1S2.ctt b/examples/pi1S2.ctt
index 561f9e3..0d827ab 100644
--- a/examples/pi1S2.ctt
+++ b/examples/pi1S2.ctt
@@ -39,6 +39,7 @@ 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 trivstwo = propPi1stwo trivstwo trivstwo
+
+test3 : Id pi1stwo trivstwo loopstwo = propPi1stwo trivstwo loopstwo
 
-test2 : Id pi1stwo trivstwo loopstwo = propPi1stwo trivstwo loopstwo
-test3 : Id pi1stwo trivstwo trivstwo = propPi1stwo trivstwo trivstwo