From: Anders Mörtberg Date: Tue, 5 May 2015 18:54:03 +0000 (+0200) Subject: Add new proof that loopS1 is a set X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=f00820846bfdb0738626e4e314c751499aa725a3;p=cubicaltt.git Add new proof that loopS1 is a set Remove unnecessary imports --- diff --git a/examples/helix.ctt b/examples/helix.ctt index cd9c127..3f24572 100644 --- a/examples/helix.ctt +++ b/examples/helix.ctt @@ -1,7 +1,6 @@ module helix where import circle -import retract import equiv encode (x:S1) (p:Id S1 base x) : helix x = subst S1 helix base x p zeroZ @@ -69,7 +68,7 @@ decodeEncodeBase : (n : Z) -> Id Z (encode base (decode base n)) n = split loopS1equalsZ : Id U loopS1 Z = isoId loopS1 Z (encode base) (decode base) decodeEncodeBase (encodeDecode base) - +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 @@ -84,7 +83,8 @@ helixSet : (x:S1) -> set (helix x) = lemPropFib (\ (x:S1) -> set (helix x)) rem 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) -setLoop : set loopS1 = retractSet loopS1 Z (encode base) (decode base) (retHelix base) ZSet +-- 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 diff --git a/examples/join.ctt b/examples/join.ctt index 62cec98..ed40ca6 100644 --- a/examples/join.ctt +++ b/examples/join.ctt @@ -1,6 +1,5 @@ module join where -import prelude import susp data join (A B:U) = inl (a:A) | inr (b:B) | pushC (a:A) (b:B) [(i=0) -> inl a, (i=1) -> inr b] diff --git a/examples/mystery.ctt b/examples/mystery.ctt index 7a88129..5712e1f 100644 --- a/examples/mystery.ctt +++ b/examples/mystery.ctt @@ -1,8 +1,5 @@ - module mystery where -import prelude -import circle import helix import torus diff --git a/examples/pi1S2.ctt b/examples/pi1s2.ctt similarity index 98% rename from examples/pi1S2.ctt rename to examples/pi1s2.ctt index 0d827ab..5eefc4b 100644 --- a/examples/pi1S2.ctt +++ b/examples/pi1s2.ctt @@ -1,4 +1,4 @@ -module pi1S2 where +module pi1s2 where import truncS2 import thm7312 diff --git a/examples/testall.ctt b/examples/testall.ctt index 0eacacd..080b0a6 100644 --- a/examples/testall.ctt +++ b/examples/testall.ctt @@ -3,18 +3,15 @@ module testall where import gradLemma import interval import uafunext2 -import helix -import susp -import ex1 -import setTrunc import prop import quotient -import torus import s2 import uafunext1 import list -import hedberg import newhedberg import other -- integer has to be after hedberg as it redefines neg import integer +import pi1s2 +import pi4s3 +import mystery diff --git a/examples/thm7312.ctt b/examples/thm7312.ctt index be9d0c4..a59e34b 100644 --- a/examples/thm7312.ctt +++ b/examples/thm7312.ctt @@ -2,7 +2,6 @@ module thm7312 where import setTrunc import groupoidTrunc -import pi import collection gTruncElim2 (A : U) (R : gTrunc A -> gTrunc A -> U) diff --git a/examples/torus.ctt b/examples/torus.ctt index 0e98f20..256d85d 100644 --- a/examples/torus.ctt +++ b/examples/torus.ctt @@ -1,6 +1,5 @@ module torus where -import prelude import circle data Torus = ptT