From: Thierry Coquand <coquand@dhcp-180153.eduroam.chalmers.se>
Date: Fri, 1 Apr 2016 10:26:27 +0000 (+0200)
Subject: study of multiplication on S1
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=68e76ef595472c9b828dfd597fd50a5b687aff8e;p=cubicaltt.git

study of multiplication on S1
---

diff --git a/examples/helix.ctt b/examples/helix.ctt
index 209cb4e..6495366 100644
--- a/examples/helix.ctt
+++ b/examples/helix.ctt
@@ -82,13 +82,6 @@ loopIt : Z -> loopS1 = split
  inl n -> itLoopNeg n
  inr n -> itLoop n
 
-test1 (n:nat) : loopS1 = transport (<i>Id S1 base (loop{S1} @ i)) (itLoop n)
-
-test (n:nat) : Z = transport (<x> helix (itLoop (suc n) @ x)) (inr zero)
-
-lemItNat (n:nat) : Id loopS1 (itLoop (suc n)) (transport (<i>Id S1 base (loop{S1} @ i)) (itLoop n)) = 
- refl loopS1 (itLoop (suc n))
-
 lemItNeg : (n:nat) -> Id loopS1  (transport (<i>Id S1 base (loop{S1} @ i)) (loopIt (inl n))) (loopIt (sucZ (inl n))) = split
  zero ->  lemInv S1 base base loop1
  suc n -> lemCompInv S1 base base base (itLoopNeg n) invLoop
@@ -112,23 +105,6 @@ lem1It : (n:Z) -> Id loopS1 (loopIt (sucZ n)) (oneTurn  (loopIt n)) = split
  inl n -> lem1ItNeg n
  inr n -> lem1ItPos n
 
-lemItPos : (n:nat) -> Id loopS1 (oneTurn (loopIt (predZ (inr n)))) (loopIt (inr n)) = split
- zero -> lemInv S1 base base loop1
- suc n -> refl loopS1 (loopIt (inr (suc n)))
-
-lemItNeg (n:nat) : Id loopS1  (oneTurn (loopIt (predZ (inl n)))) (loopIt (inl n)) = 
- lemCompInv S1 base base base (loopIt (inl n)) invLoop
-
-lemIt : (n:Z) -> Id loopS1 (oneTurn (loopIt (predZ n)))  (loopIt n) = split
- inl n -> lemItNeg n
- inr n -> lemItPos n
-
-T : U = Z -> loopS1
-p : Id U T T = <j> helix (loop{S1}@j) -> Id S1 base (loop{S1}@j)
-
-test1 : Z -> loopS1 = \ (n:Z) -> transport p loopIt n
-
-
 decode : (x:S1) -> helix x -> Id S1 base x = split
  base -> loopIt
  loop @ i -> rem @ i