From: Anders 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 = - (pP (p @ i) (transport (P (p@i /\ j)) b0) (transport (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 (Id (Id S1 base (p@i)) (decode (p@i) (encode (p@i) (p@(i/\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 (invS1 (loop2@i)) test4 : Z = winding (invS1 (compS1 loop2 loop2 @i)) -test0 : Z = winding (invMult (loop2@i) (loop2@i)) \ No newline at end of file +test0 : Z = winding (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 (Id (Id S1 base (p@i)) (decode (p@i) (encode (p@i) (p@(i/\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) (pP (p @ i) (transport ( P (p @ i /\ j)) b0) (transport ( P (p @ i \/ -j)) b1)) @ i - -- Basic data types data N0 =