From: coquand <coquand@chalmers.se>
Date: Tue, 21 Apr 2015 15:18:03 +0000 (+0200)
Subject: proof that mult is an equivalence
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=0160f7b3c8c9f896ec92ad77e4e9a1d09fff11a4;p=cubicaltt.git

proof that mult is an equivalence
---

diff --git a/examples/helix.ctt b/examples/helix.ctt
index 1c899ed..1f166a1 100644
--- a/examples/helix.ctt
+++ b/examples/helix.ctt
@@ -182,4 +182,6 @@ invMult (x y:S1) : S1 = (multIsEquiv x y).2.1
 invS1 (x:S1) : S1 = invMult x base
 
 test2 : Z = winding (<i>invS1 (loop2@i))
-test4 : Z = winding (<i>invS1 (compS1 loop2 loop2 @i))
\ No newline at end of file
+test4 : Z = winding (<i>invS1 (compS1 loop2 loop2 @i))
+
+test0 : Z = winding (<i>invMult (loop2@i) (loop2@i))
\ No newline at end of file