From 0160f7b3c8c9f896ec92ad77e4e9a1d09fff11a4 Mon Sep 17 00:00:00 2001 From: coquand Date: Tue, 21 Apr 2015 17:18:03 +0200 Subject: [PATCH] proof that mult is an equivalence --- examples/helix.ctt | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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 (invS1 (loop2@i)) -test4 : Z = winding (invS1 (compS1 loop2 loop2 @i)) \ No newline at end of file +test4 : Z = winding (invS1 (compS1 loop2 loop2 @i)) + +test0 : Z = winding (invMult (loop2@i) (loop2@i)) \ No newline at end of file -- 2.34.1