From: Anders <mortberg@chalmers.se>
Date: Wed, 6 May 2015 09:57:53 +0000 (+0200)
Subject: Clean helix
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=f958e3fe275c07e5dff11841d35b9d2b05a31aca;p=cubicaltt.git

Clean helix
---

diff --git a/examples/helix.ctt b/examples/helix.ctt
index 3f24572..3ae4584 100644
--- a/examples/helix.ctt
+++ b/examples/helix.ctt
@@ -70,22 +70,10 @@ loopS1equalsZ : Id U loopS1 Z =
 
 setLoop : set loopS1 = substInv U set loopS1 Z loopS1equalsZ ZSet
 
-lemPropF (A:U)(P:A->U)(pP:(x:A) -> prop (P x))(a0 a1:A)(p:Id A a0 a1)(b0:P a0)(b1:P a1): IdS A P a0 a1 p b0 b1 =
- <i> (pP (p @ i) (transport (<j>P (p@i /\ j)) b0) (transport (<j>P (p@i \/ -j)) b1)) @ i
-
 lemPropFib (P:S1 -> U) (pP:(x:S1) -> prop (P x)) (bP: P base) : (x:S1) -> P x = split
  base -> bP
  loop @ i -> (lemPropF S1 P pP base base loop1 bP bP) @ i
 
-helixSet : (x:S1) -> set (helix x) = lemPropFib (\ (x:S1) -> set (helix x)) rem ZSet
- where rem (x:S1) : prop (set (helix x)) = setIsProp (helix x)
-
-retHelix (x:S1) (p : Id S1 base x) : Id (Id S1 base x) (decode x (encode x p)) p = 
- transport (<i>Id (Id S1 base (p@i)) (decode (p@i) (encode (p@i) (<j>p@(i/\j)))) (<j>p@(i/\j))) (refl loopS1 triv)
-
--- Alternative proof that loopS1 is a set (requires retract.ctt):
--- setLoop' : set loopS1 = retractSet loopS1 Z (encode base) (decode base) (retHelix base) ZSet
-
 -- S1 is a groupoid
 isGroupoidS1 : groupoid S1 = lem
  where
@@ -205,4 +193,14 @@ invS1 (x:S1) : S1 = invMult x base
 test2 : Z = winding (<i>invS1 (loop2@i))
 test4 : Z = winding (<i>invS1 (compS1 loop2 loop2 @i))
 
-test0 : Z = winding (<i>invMult (loop2@i) (loop2@i))
\ No newline at end of file
+test0 : Z = winding (<i>invMult (loop2@i) (loop2@i))
+
+
+-- helixSet : (x:S1) -> set (helix x) = lemPropFib (\ (x:S1) -> set (helix x)) rem ZSet
+--  where rem (x:S1) : prop (set (helix x)) = setIsProp (helix x)
+
+-- retHelix (x:S1) (p : Id S1 base x) : Id (Id S1 base x) (decode x (encode x p)) p = 
+--  transport (<i>Id (Id S1 base (p@i)) (decode (p@i) (encode (p@i) (<j>p@(i/\j)))) (<j>p@(i/\j))) (refl loopS1 triv)
+
+-- Alternative proof that loopS1 is a set (requires retract.ctt):
+-- setLoop' : set loopS1 = retractSet loopS1 Z (encode base) (decode base) (retHelix base) ZSet
diff --git a/examples/prelude.ctt b/examples/prelude.ctt
index 9c39a43..4f8da35 100644
--- a/examples/prelude.ctt
+++ b/examples/prelude.ctt
@@ -139,7 +139,6 @@ lemPropF (A : U) (P : A -> U) (pP : (x : A) -> prop (P x)) (a0 a1 : A)
   <i> (pP (p @ i) (transport (<j> P (p @ i /\ j)) b0)
           (transport (<j> P (p @ i \/ -j)) b1)) @ i
 
-
 -- Basic data types
 
 data N0 =