From 6463e29f87f4c199fb5da1a51bd0a7cbaf1ed7c6 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Tue, 5 Jul 2016 13:35:23 +0200 Subject: [PATCH] minor changes to circle --- examples/circle.ctt | 13 ++++++++----- examples/helix.ctt | 1 + 2 files changed, 9 insertions(+), 5 deletions(-) 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 = base hmtpy : Id loopS1 ( base) ( loop{S1} @ (i /\ -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) ( 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) -- 2.34.1