Add exchange law and genPiS3

diff --git a/examples/circle.ctt b/examples/circle.ctt
index 3bd19615b9003cdb087aa7b9969cda1ae96d79ac..f12b45dfa18ece4f65e7aa9bbef86fd7225ee360 100644 (file)
--- a/examples/circle.ctt
+++ b/examples/circle.ctt
@@ -8,7 +8,7 @@ data S1 = base
 
 loopS1 : U = Id S1 base base
 
-loop1 : Id S1 base base = <i> loop{S1} @ i
+loop1 : loopS1 = <i> loop{S1} @ i
 
 invLoop : loopS1 = inv S1 base base loop1
 

diff --git a/examples/exchange.ctt b/examples/exchange.ctt
new file mode 100644 (file)
index 0000000..d3b756e
--- /dev/null
+++ b/examples/exchange.ctt
@@ -0,0 +1,135 @@
+module exchange where\r
+\r
+import susp\r
+\r
+r2 : loopS2 = refl S2 north\r
+\r
+Omega2 : U = Id loopS2 r2 r2\r
+\r
+test1 :  Omega2 =\r
+ <i j>comp S2 (merid {S2} (loop1@j)@i) \r
+     [(i=1) -> <k>merid{S2} base @-k,\r
+      (j=0) -> <k>merid{S2} base @(i/\-k),\r
+      (j=1) -> <k>merid{S2} base @(i/\-k)]\r
+\r
+compS2 (p q : loopS2) : loopS2 = compId S2 north north north p q\r
+\r
+-- horizontal and vertical composition\r
+\r
+hcomp (s t : Omega2) : Omega2 = <i j>comp S2 (s@i@j) [(i=1) -> <k> t@k@j]\r
+vcomp (s t : Omega2) : Omega2 = <i j>comp S2 (s@i@j) [(j=1) -> <k> t@i@k]\r
+\r
+-- constant square\r
+\r
+cs2 : Omega2 = refl loopS2 r2\r
+\r
+-- need to be generalized with squares\r
+\r
+Square (a0 a1 : S2) (u : Id S2 a0 a1)\r
+       (b0 b1 : S2) (v : Id S2 b0 b1)\r
+       (r0 : Id S2 a0 b0) (r1 : Id S2 a1 b1) : U\r
+  = IdP (<i> (Id S2 (u @ i) (v @ i))) r0 r1\r
+\r
+squareS2 (a0 a1:S2) (q0:Id S2 north a0) (q1:Id S2 north a1) (p0:Id S2 a0 a1) : U =\r
+ Square north a0 q0 north a1 q1 r2 p0 \r
+\r
+sqS2 (u v:loopS2) : U = Square north north u north north v r2 r2\r
+\r
+-- horizontal and vertical composition\r
+\r
+vComp  (a0 a1 a2:S2) (q0:Id S2 north a0) (q1:Id S2 north a1) (q2:Id S2 north a2)\r
+       (p0:Id S2 a0 a1) (p1:Id S2 a1 a2) (s:squareS2 a0 a1 q0 q1 p0) (s1:squareS2 a1 a2 q1 q2 p1) :\r
+       squareS2 a0 a2 q0 q2 (compId S2 a0 a1 a2 p0 p1) =\r
+ <i j>comp S2 (s@i@j) [(j=1) -> <k> s1@i@k]\r
+\r
+hComp  (a0 a1:S2) (q0 : Id S2 north a0) (q1 : Id S2 north a1) (p0 : Id S2 a0 a1) (u0 u1:loopS2)\r
+       (s : squareS2 a0 a1 q0 q1 p0) (t : sqS2 u0 u1) : \r
+  squareS2 a0 a1 (compId S2 north north a0 u0 q0) (compId S2 north north a1 u1 q1) p0 =\r
+ <i j>comp S2 (t@i@j) [(i=1) -> <k> s@k@j]\r
+\r
+-- exchange lemma\r
+\r
+compN (a:S2) (p:Id S2 north a) (q:loopS2) : Id S2 north a = compId S2 north north a q p\r
+\r
+exLem (a0 a1 a2 : S2) (q0 : Id S2 north a0) (q1:Id S2 north a1) (q2 : Id S2 north a2)\r
+      (p0 : Id S2 a0 a1) (p1: Id S2 a1 a2) (u0 u1 u2 : loopS2) \r
+      (s : squareS2 a0 a1 q0 q1 p0) (s1 : squareS2 a1 a2 q1 q2 p1) \r
+      (t : sqS2 u0 u1) (t1 : sqS2 u1 u2) : \r
+ Id (squareS2 a0 a2 (compN a0 q0 u0) (compN a2 q2 u2) (compId S2 a0 a1 a2 p0 p1))\r
+    (vComp a0 a1 a2 (compN a0 q0 u0) (compN a1 q1 u1) (compN a2 q2 u2) p0 p1\r
+                     (hComp a0 a1 q0 q1 p0 u0 u1 s t)\r
+                     (hComp a1 a2 q1 q2 p1 u1 u2 s1 t1))\r
+    (hComp a0 a2 q0 q2 (compId S2 a0 a1 a2 p0 p1) u0 u2 \r
+           (vComp a0 a1 a2 q0 q1 q2 p0 p1 s s1)\r
+           (vComp north north north u0 u1 u2 r2 r2 t t1)) = \r
+ transport \r
+ (<i> Id (squareS2 (q0@i) (q2@i) (compN (q0@i) (<j>q0@i/\j) u0) (compN (q2@i) (<j>q2@i/\j) u2) (compId S2 (q0@i) (q1@i) (q2@i) (<k>s@i@k) (<k>s1@i@k)))\r
+    (vComp (q0@i) (q1@i) (q2@i) (compN (q0@i) (<j>q0@i/\j) u0) (compN (q1@i) (<j>q1@i/\j) u1) (compN (q2@i) (<j>q2@i/\j) u2) (<k>s@i@k) (<k>s1@i@k)\r
+                     (hComp (q0@i) (q1@i) (<j>q0@i/\j) (<j>q1@i/\j) (<k>s@i@k) u0 u1 (<j k>s@i/\j@k) t)\r
+                     (hComp (q1@i) (q2@i) (<j>q1@i/\j) (<j>q2@i/\j) (<k>s1@i@k) u1 u2 (<j k>s1@i/\j@k) t1))\r
+    (hComp (q0@i) (q2@i) (<j>q0@i/\j) (<j>q2@i/\j) (compId S2 (q0@i) (q1@i) (q2@i) (<k>s@i@k) (<k>s1@i@k)) u0 u2 \r
+           (vComp (q0@i) (q1@i) (q2@i) (<j>q0@i/\j) (<j>q1@i/\j) (<j>q2@i/\j) (<k>s@i@k) (<k>s1@i@k) (<j k>s@i/\j@k) (<j k>s1@i/\j@k))\r
+           (vComp north north north u0 u1 u2 r2 r2 t t1)))\r
+    (refl (sqS2 u0 u2) (vComp north north north u0 u1 u2 r2 r2 t t1))\r
+\r
+corExLem (t t1 s s1 : Omega2) :\r
+ Id Omega2 (vcomp (hcomp t s) (hcomp t1 s1)) (hcomp (vcomp t t1) (vcomp s s1)) = \r
+ exLem north north north r2 r2 r2 r2 r2 r2 r2 r2 s s1 t t1\r
+\r
+-- we should be able to deduce that vcomp t s = hcomp t s\r
+\r
+rR2 : Omega2 = refl loopS2 r2\r
+\r
+lemIdl (A:U) (a b:A) (p:Id A a b) : Id (Id A a b) (compId A a a b (refl A a) p) p = \r
+ transport (<i>Id (Id A a (p@i)) (compId A a a (p@i) (refl A a) (<j>p@i/\j)) (<j>p@i/\j))\r
+           (refl (Id A a a) (refl A a))\r
+\r
+lemRV (s:Omega2) : Id Omega2 (vcomp rR2 s) s = <k i j>lemIdl S2 north north (s@i)@k@j\r
+\r
+lemRH (s:Omega2) : Id Omega2 (hcomp rR2 s) s = <k i j>lemIdl S2 north north (<l>s@l@j)@k@i\r
+\r
+lem1 (s t:Omega2) : Id Omega2 (vcomp t s) (hcomp t s) = \r
+ compId Omega2 (vcomp t s) (hcomp t (vcomp rR2 s)) (hcomp t s) \r
+   (compId Omega2 (vcomp t s) (vcomp (hcomp t rR2) (hcomp rR2 s)) (hcomp t (vcomp rR2 s)) rem1 rem2)\r
+    rem3\r
+ where\r
+ rem1 : Id Omega2 (vcomp t s) (vcomp (hcomp t rR2) (hcomp rR2 s)) =  <i>vcomp t (lemRH s@-i)\r
+ rem2 : Id Omega2 (vcomp (hcomp t rR2) (hcomp rR2 s)) (hcomp t (vcomp rR2 s)) =  corExLem t rR2 rR2 s\r
+ rem3 : Id Omega2 (hcomp t (vcomp rR2 s)) (hcomp t s) =  <i>hcomp t (lemRV s@i)\r
+\r
+lemInv (A:U) (a b:A) (p:Id A a b) : Id (Id A a a) (compId A a b a p (<i>p@-i)) (refl A a) =\r
+ transport (<i>Id (Id A a a) (compId A a (p@i) a (<j>p@i/\j) (<j>p@i/\-j)) (refl A a)) (refl (Id A a a) (refl A a))\r
+\r
+g2 : Omega2 = test1\r
+invG2 : Omega2 = <i j>g2@i@-j\r
+\r
+-- lem2 : Id Omega2 (hcomp g2 invG2) rR2 = <k i j>lemInv S2 north north (<l>g2@l@j)@k@i\r
+\r
+lem3 : Id Omega2 (vcomp g2 invG2) rR2 = <k i j>lemInv S2 north north (g2@i)@k@j\r
+--  compId Omega2 (vcomp g2 invG2) (hcomp h2 invG2) rR2 (lem1 g2 invG2) lem2\r
+\r
+lemInv1 (A:U) (a b:A) (p:Id A a b) : Id (Id A b b) (compId A b a b (<i>p@-i) p) (refl A b) =\r
+ transport (<i>Id (Id A b b) (compId A b (p@-i) b (<j>p@-i\/-j) (<j>p@-i\/j)) (refl A b)) (refl (Id A b b) (refl A b))\r
+\r
+lem4 : Id Omega2 (vcomp invG2 g2) rR2 = <k i j>lemInv1 S2 north north (g2@i)@k@j\r
+\r
+-- commutativity\r
+\r
+lem5 (s t:Omega2) : Id Omega2 (vcomp t s) (vcomp s t) =\r
+ compId Omega2 (vcomp t s) (vcomp (hcomp rR2 s) t) (vcomp s t)\r
+  (compId Omega2 (vcomp t s) (hcomp (vcomp rR2 t) s) (vcomp (hcomp rR2 s) t) \r
+   (compId Omega2 (vcomp t s) (hcomp t s) (hcomp (vcomp rR2 t) s) (lem1 s t) rem4)\r
+    rem5)\r
+   rem6\r
+ where\r
+ rem4 : Id Omega2 (hcomp t s) (hcomp (vcomp rR2 t) s) = <i>hcomp (lemRV t@-i) s\r
+ rem5 : Id Omega2 (hcomp (vcomp rR2 t) s) (vcomp (hcomp rR2 s) t) = <i>corExLem rR2 t s rR2@-i\r
+ rem6 : Id Omega2 (vcomp (hcomp rR2 s) t) (vcomp s t) = <i>vcomp (lemRH s@i) t\r
+\r
+genPi3S2 : Id Omega2 rR2 rR2 = \r
+ compId Omega2 rR2 (vcomp invG2 g2) rR2 (compId Omega2 rR2 (vcomp g2 invG2) (vcomp invG2 g2) rem1 rem2) lem4\r
+ where\r
+  rem1 : Id Omega2 rR2 (vcomp g2 invG2) = <i>lem3@-i\r
+  rem2 : Id Omega2 (vcomp g2 invG2) (vcomp invG2 g2) = lem5 invG2 g2\r
+\r
+\r

diff --git a/examples/pi1s2.ctt b/examples/pi1s2.ctt
index 5eefc4be5dd6790dcb8b7b755a23fb1b4cc025a8..8ac43949e44f741f51dc4564688134da20de26a5 100644 (file)
--- a/examples/pi1s2.ctt
+++ b/examples/pi1s2.ctt
@@ -3,7 +3,7 @@ module pi1s2 where
 import truncS2
 import thm7312
 
-pi1S2 : U = sTrunc (Id S2 north north) 
+pi1S2 : U = sTrunc loopS2
 
 incN : gTrunc S2 = inc north
 

diff --git a/examples/pi4s3.ctt b/examples/pi4s3.ctt
index 9b17e30cad932310ae8220282aa2837ad35b2db9..82b1d85bfc4489c9967d6fc553233d78e238ca06 100644 (file)
--- a/examples/pi4s3.ctt
+++ b/examples/pi4s3.ctt
@@ -2,6 +2,7 @@ module pi4s3 where
 
 import join
 import hopf
+import exchange
 
 ptJoin (pA : ptType) (B:U) : ptType = (join pA.1 B, inl (pt pA))
 
@@ -87,3 +88,6 @@ test0To4 : (itOmega three ptS2).1 = f4 test0To3
 
 -- NOT SURE (takes a long time)
 test0To5 : (itOmega three (ptJoin ptS1 S1)).1 = f5 test0To4
+
+-- Test f5 on a generator given by the exchange law
+testf5 : (itOmega three (ptJoin ptS1 S1)).1 = f5 genPi3S2
\ No newline at end of file

diff --git a/examples/susp.ctt b/examples/susp.ctt
index 5d219cec7c7c9d74567b5e575e6db1b20164ae7a..20a80c92681b66a8e52de0556080b68e013672cd 100644 (file)
--- a/examples/susp.ctt
+++ b/examples/susp.ctt
@@ -96,3 +96,8 @@ loop2S : Id sone north north = compId sone north north north loop1S loop1S
 test0S : Z = windingS (refl sone north)\r
 \r
 test2S : Z = windingS loop2S\r
+\r
+-- The sphere is the suspension of the circle:\r
+S2 : U = susp S1\r
+\r
+loopS2 : U = Id S2 north north\r

diff --git a/examples/truncS2.ctt b/examples/truncS2.ctt
index e1003e2d6081a4b829b9b43df1bc1a7d599add7d..b6a1aa4b275e6367f5f7cefdd55a8b4341472e78 100644 (file)
--- a/examples/truncS2.ctt
+++ b/examples/truncS2.ctt
@@ -18,8 +18,6 @@ lemLoopSet (X:U) (sX: set X) : Id U (aLoop X) X
 lemS1Set (X : U) (sX: set X) : Id U (S1 -> X) X =
  compId U (S1 -> X) (aLoop X) X (<i>thm X@-i) (lemLoopSet X sX)
 
-S2 : U = susp S1
-
 lemGrp1 (X : U) (gX: groupoid X) : Id U (suspOf S1 X) ((u:X) * (v : X) * Id X u v)
    = <i> (u:X) * (v:X) * (lemS1Set (Id X u v) (gX u v) @ i)