add 5th winding number

diff --git a/examples/circle.ctt b/examples/circle.ctt
index 62544321d16eb0364f97522e7a3e1117a2ab09c8..30a8d3b5829b26aac2f095fb53d739d6177171d7 100644 (file)
--- 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