From: Anders Mörtberg <andersmortberg@gmail.com>
Date: Tue, 5 Jul 2016 11:35:23 +0000 (+0200)
Subject: minor changes to circle
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=6463e29f87f4c199fb5da1a51bd0a7cbaf1ed7c6;p=cubicaltt.git

minor changes to circle
---

diff --git a/examples/circle.ctt b/examples/circle.ctt
index 59c608a..040a01a 100644
--- a/examples/circle.ctt
+++ b/examples/circle.ctt
@@ -65,9 +65,12 @@ triv : loopS1 = <i> base
 hmtpy : Id loopS1 (<i> base) (<i> loop{S1} @ (i /\ -i)) =
   <j i> loop{S1} @ j /\ i /\ -i
 
+circleelim (X : U) (x : X) (p : Id X x x) : S1 -> X = split
+  base -> x
+  loop @ i -> p @ i
 
--- the loop space of the circle is equal to Z
-
--- loopS1equalsZ : Id U loopS1 Z = undefined
---  isoId loopS1 Z (encode base) (decode base) decodeEncodeBase (encodeDecode base)
-
+apcircleelim (A B : U) (x : A) (p : Id A x x) (f : A -> B) :
+  (z : S1) -> Id B (f (circleelim A x p z))
+                   (circleelim B (f x) (<i> f (p @ i)) z) = split
+   base -> <_> f x
+   loop @ i -> <_> f (p @ i)
diff --git a/examples/helix.ctt b/examples/helix.ctt
index 07876e9..8a31c57 100644
--- a/examples/helix.ctt
+++ b/examples/helix.ctt
@@ -171,6 +171,7 @@ decodeEncodeBase : (n : Z) -> Id Z (encode base (decode base n)) n = split
   inl n -> decodeEncodeBaseNeg n
   inr n -> decodeEncodeBasePos n
 
+-- the loop space of the circle is equal to Z
 loopS1equalsZ : Id U loopS1 Z = 
   isoId loopS1 Z (encode base) (decode base) decodeEncodeBase (encodeDecode base)