piS2 is trivial

diff --git a/examples/deppath.ctt b/examples/deppath.ctt
new file mode 100644 (file)
index 0000000..3a529bd
--- /dev/null
+++ b/examples/deppath.ctt
@@ -0,0 +1,15 @@
+module deppath where
+
+import prelude
+
+funDepTr (A0 A1 :U) (p:Id U A0 A1) (u0:A0) (u1:A1) :
+             Id U (IdP p u0 u1) (Id A1 (transport p u0) u1) =
+ <i> IdP (<l> p @ (i\/l)) (transport (<l> p @ (i/\l)) u0) u1
+
+funDepTrInv (A0 A1 :U) (p:Id U A0 A1) (u0:A0) (u1:A1) :
+             Id U (Id A0 u0 (transport (<i>p@-i) u1)) (IdP p u0 u1) =
+ <i> IdP (<l> p @ (i/\l)) u0 (transport (<l> p @ (i\/-l)) u1)
+
+funDep (A0 A1 :U) (p:Id U A0 A1) (u0:A0) (u1:A1) :
+      Id U (Id A0 u0 (transport (<i>p@-i) u1)) (Id A1 (transport p u0) u1) =
+ <i> Id (p @ i) (transport (<l> p @ (i/\l)) u0) (transport (<l> p @ (i\/-l)) u1)
\ No newline at end of file

diff --git a/examples/pi1S2.ctt b/examples/pi1S2.ctt
index 9c3c0a02341f6b4674b432d4c810ff5cdf330ee8..e79d97bb72fa9905d47dba1c8ba43374b0fabe87 100644 (file)
--- a/examples/pi1S2.ctt
+++ b/examples/pi1S2.ctt
@@ -1,47 +1,30 @@
 module pi1S2 where
 
 import truncS2
-import susp
-import groupoidTrunc
+import thm7312
 
-lemGrp4 (X : U) (gX:groupoid X) : Id U (gTrunc S2 -> X) X
- = compId U (gTrunc S2 -> X) (S2 -> X) X (univG S2 X gX) (lemGrp3 X gX)
+pi1S2 : U = sTrunc (Id S2 north north) 
 
-corr : Id U (gTrunc S2 -> gTrunc S2) (gTrunc S2) = lemGrp4 (gTrunc S2) (gTr S2)
+incN : gTrunc S2 = inc north
 
-lemTransport (A B :U) (p : Id U A B) (a0 a1 : A) (h: Id B (transport p a0) (transport p a1)) : Id A a0 a1 =
- transport (<i>Id (p@-i) (transport (<j>p@(-i/\j)) a0) (transport (<j>p@(-i/\j)) a1)) h
+cor7312 : Id U pi1S2 (Id (gTrunc S2) incN incN) =
+ thm7312 S2 north north
 
+propPi1S2 : prop pi1S2 =
+ substInv U prop pi1S2 (Id (gTrunc S2) incN incN)  cor7312
+    (propSet (gTrunc S2) propgTruncS2 incN incN)
 
-corr1 : Id (gTrunc S2 -> gTrunc S2) (\ (x:gTrunc S2) -> x) (\ (x:gTrunc S2) -> inc north) =
- lemTransport (gTrunc S2 -> gTrunc S2) (gTrunc S2) corr 
-              (\ (x:gTrunc S2) -> x) (\ (x:gTrunc S2) -> inc north) (refl (gTrunc S2) (inc north))
+meridS2 : Id S2 north south = <i>merid{S2} base@i
 
-corr2 (x:gTrunc S2) : Id (gTrunc S2) x (inc north) = <i> corr1@i x 
+trivS2 : pi1S2 = inc (refl S2 north)
+loopS2 : pi1S2 = inc (compId S2 north south north meridS2 (<i>meridS2@-i))
 
-test : Id (gTrunc S2) (inc south) (inc north) = corr2 (inc south)
+test : Id pi1S2 trivS2 loopS2 = propPi1S2 trivS2 loopS2
+test1 : Id pi1S2 trivS2 trivS2 = propPi1S2 trivS2 trivS2
 
--- normal form
+-- we can transport this since S1 = susp bool
 
-test : Id (gTrunc S2) (inc south) (inc north) = 
- <i> inc (comp S2 north 
-         [ (i = 0) -> <j> comp S2 south 
-          [ (j = 0) -> <k> comp S2 north
-           [ (k = 0) -> <l> comp S2 south
-            [ (l = 0) -> <m> comp S2 north
-             [ (m = 0) -> <n> comp S2 south 
-              [ (n = 0) -> <p> comp S2 north 
-               [ (p = 0) -> <q> comp S2 north [ (q = 1) -> <r> merid {S2} base @ r ] ] ] ] ] ] ] ])
+eqS1
 
+eqS2 : Id U S2 stwo = subst U susp S1 sone (<i>s1EqCircle@-i)
 
-
-test1 : Id (gTrunc S2) (inc north) (inc north) = corr2 (inc north)
-
--- this should imply that any element in gTrunc (susp sone) is equal to inc north
-
-stwo : U = susp sone
-
-corr3 : (x:gTrunc stwo) -> Id (gTrunc stwo) x (inc north) =
- transport (<i>(x:gTrunc (susp (s1EqCircle@-i))) -> Id (gTrunc (susp (s1EqCircle@-i))) x (inc north)) corr2
-
-test2 : Id (gTrunc stwo) (inc south) (inc north) = corr3 (inc south)

diff --git a/examples/thm7312.ctt b/examples/thm7312.ctt
new file mode 100644 (file)
index 0000000..be9d0c4
--- /dev/null
+++ b/examples/thm7312.ctt
@@ -0,0 +1,96 @@
+module thm7312 where
+
+import setTrunc
+import groupoidTrunc
+import pi
+import collection
+
+gTruncElim2 (A : U) (R : gTrunc A -> gTrunc A -> U)
+            (tR : (x y : gTrunc A) -> groupoid (R x y))
+            (g:(a b : A) -> R (inc a) (inc b)) : (x y : gTrunc A) -> R x y =
+ gTruncElim A P tP hP
+ where
+  P (x: gTrunc A) : U = (y : gTrunc A) -> R x y
+  tP (x : gTrunc A) : groupoid (P x) = groupoidPi (gTrunc A) (R x) (tR x)
+  hP (a : A) : P (inc a) = gTruncElim A (R (inc a)) (tR (inc a)) (g a)
+
+-- Theorem 7.3.12
+thm7312 (A : U) (x y : A) : Id U (sTrunc (Id A x y))
+                                 (Id (gTrunc A) (inc x) (inc y)) = lem3 (inc x) (inc y)
+  where
+  tA : U = gTrunc A
+
+  tAtrunc : groupoid tA = gTr A
+
+  P : tA -> tA -> SET
+    = gTruncElim2 A (\ (z t: tA) -> SET) (\ (x t:tA) -> groupoidSET)
+                    (\ (x y:A) -> (sTrunc (Id A x y),sTr (Id A x y)))
+
+  Q (u v: tA) : U = (P u v).1
+
+  encode : (u v : tA) -> Q u v -> Id tA u v
+   = gTruncElim2 A (\(u v:tA) -> Q u v -> Id tA u v)
+                   (\(u v:tA) -> setGroupoid (Q u v -> Id tA u v) (setFun (Q u v) (Id tA u v) (tAtrunc u v)))
+                   rem
+    where
+     rem (x y : A) : sTrunc (Id A x y) -> Id tA (inc x) (inc y)
+             = sTruncRec (Id A x y) (Id tA (inc x) (inc y)) (tAtrunc (inc x) (inc y))
+                         (\ (p:Id A x y) -> <i>inc (p@i))
+
+
+  test (x : A) : Id U (Q (inc x) (inc x)) (sTrunc (Id A x x)) = refl U (sTrunc (Id A x x))
+
+  r : (u : tA) -> Q u u
+    = gTruncElim A (\ (u:tA) -> Q u u) rem1 rem
+    where
+     rem1 (u : tA) : groupoid (Q u u) = setGroupoid (Q u u) (P u u).2
+     rem (x : A) : sTrunc (Id A x x) = inc (refl A x)
+
+  decode (u v : tA) (p:Id tA u v) : Q u v = subst tA (Q u) u v p (r u) -- J tA u (\v p -> Q u v) (r u)
+
+  lem1 (u :tA) : (v : tA) (p : Id tA u v) -> Id (Id tA u v) (encode u v (decode u v p)) p
+   = J tA u (\(v : tA) (p : Id tA u v) -> Id (Id tA u v) (encode u v (decode u v p)) p) (rem u)
+    where
+     T (u : tA) : U = Id (Id tA u u) (encode u u (decode u u (refl tA u))) (refl tA u)
+
+     truncT (u : tA) : groupoid (T u) =
+      setGroupoid (T u) (rem (encode u u (decode u u (refl tA u))) (refl tA u))
+       where
+        rem : groupoid (Id tA u u) = setGroupoid (Id tA u u) (tAtrunc u u)
+
+     rem : (u : tA) -> T u = gTruncElim A T truncT (\ (x:A) -> refl (Id tA (inc x) (inc x)) (refl tA (inc x)))
+
+
+  lem2 : (u v : tA) (p : Q u v) -> Id (Q u v) (decode u v (encode u v p)) p
+    = gTruncElim2 A R tR rem
+    where
+     R (u v : tA) : U = (p : Q u v) -> Id (Q u v) (decode u v (encode u v p)) p
+
+     tR (u v : tA) : groupoid (R u v)
+       = groupoidPi (Q u v) (\ (p:Q u v) -> Id (Q u v) (decode u v (encode u v p)) p) rem1
+       where
+        rem : groupoid (Q u v) = setGroupoid (Q u v) (P u v).2
+        rem1 (p : Q u v) : groupoid (Id (Q u v) (decode u v (encode u v p)) p)
+         = setGroupoid (Id (Q u v) (decode u v (encode u v p)) p) (rem (decode u v (encode u v p)) p)
+
+     rem1 (x:A) : (y : A) (p : Id A x y) ->
+            Id (sTrunc (Id A x y)) (decode (inc x) (inc y) (encode (inc x) (inc y) (inc p))) (inc p)
+       = J A x (\ (y:A) (p:Id A x y) -> 
+                 Id (sTrunc (Id A x y)) (decode (inc x) (inc y) (encode (inc x) (inc y) (inc p))) (inc p)) rem2
+       where
+        rem2 : Id (sTrunc (Id A x x)) (decode (inc x) (inc x) (encode (inc x) (inc x) (inc (refl A x)))) (inc (refl A x))
+            = refl (sTrunc (Id A x x)) (inc (refl A x)) 
+
+     rem (x y : A) : (p : sTrunc (Id A x y)) ->
+           Id (sTrunc (Id A x y)) (decode (inc x) (inc y) (encode (inc x) (inc y) p)) p
+        = sTruncElim (Id A x y) T tT (rem1 x y)
+       where
+        T (p: sTrunc (Id A x y)) : U = Id (sTrunc (Id A x y)) (decode (inc x) (inc y) (encode (inc x) (inc y) p)) p
+
+        tT (p : sTrunc (Id A x y)) : set (T p)
+          = setGroupoid (sTrunc (Id A x y)) (sTr (Id A x y))
+                        (decode (inc x) (inc y) (encode (inc x) (inc y) p)) p
+
+
+  lem3 (u v : tA) : Id U (Q u v) (Id tA u v) =
+     isoId (Q u v) (Id tA u v) (encode u v) (decode u v) (lem1 u v) (lem2 u v)

diff --git a/examples/truncS2.ctt b/examples/truncS2.ctt
index 6349b8cef207cd27878375425c2618a2bd1cde25..e1003e2d6081a4b829b9b43df1bc1a7d599add7d 100644 (file)
--- a/examples/truncS2.ctt
+++ b/examples/truncS2.ctt
@@ -2,6 +2,8 @@ module truncS2 where
 
 import ex1
 import indSusp
+import susp
+import groupoidTrunc
 
 -- is X is a set then Id U (aLoop X) X
 
@@ -35,4 +37,63 @@ lemGrp2 (X : U) (gX:groupoid X) : Id U (suspOf S1 X) X =
 lemGrp3 (X : U) (gX: groupoid X) : Id U (S2 -> X) X =
  compId U (S2 -> X) (suspOf S1 X) X (funSusp S1 X) (lemGrp2 X gX)
 
-test (X:U) (gX: groupoid X) (f:S2 -> X) : X = transport (lemGrp3 X gX) f
\ No newline at end of file
+test (X:U) (gX: groupoid X) (f:S2 -> X) : X = transport (lemGrp3 X gX) f
+
+lemGrp4 (X : U) (gX:groupoid X) : Id U (gTrunc S2 -> X) X
+ = compId U (gTrunc S2 -> X) (S2 -> X) X (univG S2 X gX) (lemGrp3 X gX)
+
+corr : Id U (gTrunc S2 -> gTrunc S2) (gTrunc S2) = lemGrp4 (gTrunc S2) (gTr S2)
+
+lemTransport (A B :U) (p : Id U A B) (a0 a1 : A) (h: Id B (transport p a0) (transport p a1)) : Id A a0 a1 =
+ transport (<i>Id (p@-i) (transport (<j>p@(-i/\j)) a0) (transport (<j>p@(-i/\j)) a1)) h
+
+
+corr1 : Id (gTrunc S2 -> gTrunc S2) (\ (x:gTrunc S2) -> x) (\ (x:gTrunc S2) -> inc north) =
+ lemTransport (gTrunc S2 -> gTrunc S2) (gTrunc S2) corr 
+              (\ (x:gTrunc S2) -> x) (\ (x:gTrunc S2) -> inc north) (refl (gTrunc S2) (inc north))
+
+corr2 (x:gTrunc S2) : Id (gTrunc S2) x (inc north) = <i> corr1@i x 
+
+propgTruncS2 : prop (gTrunc S2) =
+ \ (x y : gTrunc S2) -> compId (gTrunc S2) x (inc north) y (corr2 x) (<i>corr2 y@-i)
+
+
+test : Id (gTrunc S2) (inc south) (inc north) = corr2 (inc south)
+
+-- normal form
+
+test : Id (gTrunc S2) (inc south) (inc north) = 
+ <i> inc (comp S2 north 
+         [ (i = 0) -> <j> comp S2 south 
+          [ (j = 0) -> <k> comp S2 north
+           [ (k = 0) -> <l> comp S2 south
+            [ (l = 0) -> <m> comp S2 north
+             [ (m = 0) -> <n> comp S2 south 
+              [ (n = 0) -> <p> comp S2 north 
+               [ (p = 0) -> <q> comp S2 north [ (q = 1) -> <r> merid {S2} base @ r ] ] ] ] ] ] ] ])
+
+test1 : Id (gTrunc S2) (inc north) (inc north) = corr2 (inc north)
+
+test1 : Id (gTrunc S2) (inc north) (inc north) = compId (gTrunc S2) (inc north) (inc south) (inc north) (<i>test@-i) test
+
+-- this should imply that any element in gTrunc (susp sone) is equal to inc north
+
+stwo : U = susp sone
+
+corr3 : (x:gTrunc stwo) -> Id (gTrunc stwo) x (inc north) =
+ transport (<i>(x:gTrunc (susp (s1EqCircle@-i))) -> Id (gTrunc (susp (s1EqCircle@-i))) x (inc north)) corr2
+
+test2 : Id (gTrunc stwo) (inc south) (inc north) = corr3 (inc south)
+
+-- normal form
+
+test2 : Id (gTrunc stwo) (inc south) (inc north) = 
+ <i> inc (comp stwo north 
+     [ (i = 0) -> <j> comp stwo south 
+      [ (j = 0) -> <k> comp stwo north 
+       [ (k = 0) -> <l> comp stwo south 
+        [ (l = 0) -> <m> comp stwo north 
+         [ (m = 0) -> <n> comp stwo south 
+          [ (n = 0) -> <p> comp stwo north 
+           [ (p = 0) -> <q> comp stwo north 
+            [ (q = 1) -> <r> merid {stwo} north @ r ] ] ] ] ] ] ] ])