study of multiplication on S1

diff --git a/examples/helix.ctt b/examples/helix.ctt
index 209cb4e6a3db9adce943155a247840a4451d7b89..64953666060309fd6bed83a9f25ac3d65d55ff9b 100644 (file)
--- 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