From: Anders Mörtberg 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 = merid{stwo} south@i trivstwo : pi1stwo = inc (refl stwo north) loopstwo : pi1stwo = inc (compId stwo north south north meridNstwo (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