simple computation using multZ

diff --git a/examples/torsor.ctt b/examples/torsor.ctt
index 2f2ad37917e12ec136faa4461eb404a1411510fb..2983ab1095ea2dd7ae18db3054a847a6cc3320b8 100644 (file)
--- a/examples/torsor.ctt
+++ b/examples/torsor.ctt
@@ -851,5 +851,11 @@ doubleLoopBZ : loopBZ -> loopBZ = transport (<i> loopS1equalsLoopBZ@i -> loopS1e
 -- Time: 0m25.191s\r
 \r
 -- > let visible_all in let doubleLoop : Id BZ (multZ ZBZ ZBZ) (multZ ZBZ ZBZ) = <i> multZ (loopZ@-i) (loopZ@i) in transport (<j> BZSet (transport (<i> BZSet (doubleLoop @ i)) (<_> ZBZ) @ j)) zeroZ\r
+-- too slow\r
+\r
+-- > let visible_all in transport (<j> BZSet (transport (<i> BZSet (multZ (loopZ@-i) (loopZ@i))) (<_> ZBZ) @ j)) zeroZ\r
+-- EVAL: inr (suc (suc zero))\r
+\r
+-- multS1 : S1 -> S1 -> S1 = transport (<i> S1equalsBZ@-i -> S1equalsBZ@-i -> S1equalsBZ@-i) multZ\r
 \r
 visible_all\r