Add new proof that loopS1 is a set

Remove unnecessary imports

diff --git a/examples/helix.ctt b/examples/helix.ctt
index cd9c1273dc140899ba8e9c1a901701268a1e5a17..3f24572961635b1c7eae3cf650e57267260096f3 100644 (file)
--- 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 =
  <i> (pP (p @ i) (transport (<j>P (p@i /\ j)) b0) (transport (<j>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 (<i>Id (Id S1 base (p@i)) (decode (p@i) (encode (p@i) (<j>p@(i/\j)))) (<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 62cec98caf053f5e74daad0a85d9c43659eb5784..ed40ca64ba48e63ebfde0a1967eb0bde71d0757d 100644 (file)
--- a/examples/join.ctt
+++ b/examples/join.ctt
@@ -1,6 +1,5 @@
 module join where\r
 \r
-import prelude\r
 import susp\r
 \r
 data join (A B:U) = inl (a:A) | inr (b:B) | pushC (a:A) (b:B) <i> [(i=0) -> inl a, (i=1) -> inr b]\r

diff --git a/examples/mystery.ctt b/examples/mystery.ctt
index 7a88129d9c3d31c28067304faaf6060fe8863308..5712e1f3342877cab7399b41bd957231bfac233a 100644 (file)
--- 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 0d827ab8e0555b73fb8f590474eda44f3c335409..5eefc4be5dd6790dcb8b7b755a23fb1b4cc025a8 100644 (file)
--- 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 0eacacd0bc211b9f73290b2af00a36c6b6ec9129..080b0a69dd1bce35194bad9bc00f55b6150a19d7 100644 (file)
--- 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 be9d0c4eb4de58abaa7ddec6ce05133f5fcce479..a59e34b04128a03bd3f3a4f1bf68b7061126b1c6 100644 (file)
--- 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 0e98f203aba30bc622b9a0c284451b9eb3234cbc..256d85d0be2f8c0270440e750b82275232e66252 100644 (file)
--- a/examples/torus.ctt
+++ b/examples/torus.ctt
@@ -1,6 +1,5 @@
 module torus where
 
-import prelude
 import circle
 
 data Torus = ptT