From: Rafaël Bocquet <rafael.bocquet@ens.fr>
Date: Thu, 14 Apr 2016 12:17:08 +0000 (+0200)
Subject: simple computation using multZ
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=d83e672abd36013b3b920ff95cb2c12f1c1f224f;p=cubicaltt.git

simple computation using multZ
---

diff --git a/examples/torsor.ctt b/examples/torsor.ctt
index 2f2ad37..2983ab1 100644
--- a/examples/torsor.ctt
+++ b/examples/torsor.ctt
@@ -851,5 +851,11 @@ doubleLoopBZ : loopBZ -> loopBZ = transport (<i> loopS1equalsLoopBZ@i -> loopS1e
 -- Time: 0m25.191s
 
 -- > 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
+-- too slow
+
+-- > let visible_all in transport (<j> BZSet (transport (<i> BZSet (multZ (loopZ@-i) (loopZ@i))) (<_> ZBZ) @ j)) zeroZ
+-- EVAL: inr (suc (suc zero))
+
+-- multS1 : S1 -> S1 -> S1 = transport (<i> S1equalsBZ@-i -> S1equalsBZ@-i -> S1equalsBZ@-i) multZ
 
 visible_all