proof that mult is an equivalence

diff --git a/examples/helix.ctt b/examples/helix.ctt
index 1c899ede0cef4b22abcbfd960727330ef7df6031..1f166a19e7ab4412b338e805cce17e88e35b6bbb 100644 (file)
--- 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