From: Anders Mörtberg <mortberg@chalmers.se>
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 =
  <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 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> [(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