From: Anders Mörtberg Date: Thu, 19 Apr 2018 14:00:18 +0000 (-0400) Subject: add 5th winding number X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=d2cd0444d0cc5349fdf42892e644de7ab17cee81;p=cubicaltt.git add 5th winding number --- diff --git a/examples/circle.ctt b/examples/circle.ctt index 6254432..30a8d3b 100644 --- a/examples/circle.ctt +++ b/examples/circle.ctt @@ -39,6 +39,7 @@ loopZ2 : Z = winding (compS1 loop1 loop1) loopZ3 : Z = winding (compS1 loop1 (compS1 loop1 loop1)) loopZN1 : Z = winding invLoop loopZ0 : Z = winding (compS1 loop1 invLoop) +loopZ5 : Z = winding (compS1 loop1 (compS1 loop1 (compS1 loop1 (compS1 loop1 loop1)))) mLoop : (x : S1) -> Path S1 x x = split base -> loop1