minor changes to circle

diff --git a/examples/circle.ctt b/examples/circle.ctt
index 59c608a882952f98316da451fe444ce4db341c47..040a01abcffab8a7960246fc34a851c1fff260eb 100644 (file)
--- 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 07876e9abec410ff201d5dc1e4693360dab44265..8a31c578dc37ef8d082bb1822a5031d361b38047 100644 (file)
--- 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)