From 4283a392f9d7feb64859b4c3e11550e2387ce3c8 Mon Sep 17 00:00:00 2001 From: Anders Date: Fri, 8 May 2015 15:29:25 +0200 Subject: [PATCH] Add exchange law and genPiS3 --- examples/circle.ctt | 2 +- examples/exchange.ctt | 135 ++++++++++++++++++++++++++++++++++++++++++ examples/pi1s2.ctt | 2 +- examples/pi4s3.ctt | 4 ++ examples/susp.ctt | 5 ++ examples/truncS2.ctt | 2 - 6 files changed, 146 insertions(+), 4 deletions(-) create mode 100644 examples/exchange.ctt diff --git a/examples/circle.ctt b/examples/circle.ctt index 3bd1961..f12b45d 100644 --- 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 = loop{S1} @ i +loop1 : loopS1 = loop{S1} @ i invLoop : loopS1 = inv S1 base base loop1 diff --git a/examples/exchange.ctt b/examples/exchange.ctt new file mode 100644 index 0000000..d3b756e --- /dev/null +++ b/examples/exchange.ctt @@ -0,0 +1,135 @@ +module exchange where + +import susp + +r2 : loopS2 = refl S2 north + +Omega2 : U = Id loopS2 r2 r2 + +test1 : Omega2 = + comp S2 (merid {S2} (loop1@j)@i) + [(i=1) -> merid{S2} base @-k, + (j=0) -> merid{S2} base @(i/\-k), + (j=1) -> merid{S2} base @(i/\-k)] + +compS2 (p q : loopS2) : loopS2 = compId S2 north north north p q + +-- horizontal and vertical composition + +hcomp (s t : Omega2) : Omega2 = comp S2 (s@i@j) [(i=1) -> t@k@j] +vcomp (s t : Omega2) : Omega2 = comp S2 (s@i@j) [(j=1) -> t@i@k] + +-- constant square + +cs2 : Omega2 = refl loopS2 r2 + +-- need to be generalized with squares + +Square (a0 a1 : S2) (u : Id S2 a0 a1) + (b0 b1 : S2) (v : Id S2 b0 b1) + (r0 : Id S2 a0 b0) (r1 : Id S2 a1 b1) : U + = IdP ( (Id S2 (u @ i) (v @ i))) r0 r1 + +squareS2 (a0 a1:S2) (q0:Id S2 north a0) (q1:Id S2 north a1) (p0:Id S2 a0 a1) : U = + Square north a0 q0 north a1 q1 r2 p0 + +sqS2 (u v:loopS2) : U = Square north north u north north v r2 r2 + +-- horizontal and vertical composition + +vComp (a0 a1 a2:S2) (q0:Id S2 north a0) (q1:Id S2 north a1) (q2:Id S2 north a2) + (p0:Id S2 a0 a1) (p1:Id S2 a1 a2) (s:squareS2 a0 a1 q0 q1 p0) (s1:squareS2 a1 a2 q1 q2 p1) : + squareS2 a0 a2 q0 q2 (compId S2 a0 a1 a2 p0 p1) = + comp S2 (s@i@j) [(j=1) -> s1@i@k] + +hComp (a0 a1:S2) (q0 : Id S2 north a0) (q1 : Id S2 north a1) (p0 : Id S2 a0 a1) (u0 u1:loopS2) + (s : squareS2 a0 a1 q0 q1 p0) (t : sqS2 u0 u1) : + squareS2 a0 a1 (compId S2 north north a0 u0 q0) (compId S2 north north a1 u1 q1) p0 = + comp S2 (t@i@j) [(i=1) -> s@k@j] + +-- exchange lemma + +compN (a:S2) (p:Id S2 north a) (q:loopS2) : Id S2 north a = compId S2 north north a q p + +exLem (a0 a1 a2 : S2) (q0 : Id S2 north a0) (q1:Id S2 north a1) (q2 : Id S2 north a2) + (p0 : Id S2 a0 a1) (p1: Id S2 a1 a2) (u0 u1 u2 : loopS2) + (s : squareS2 a0 a1 q0 q1 p0) (s1 : squareS2 a1 a2 q1 q2 p1) + (t : sqS2 u0 u1) (t1 : sqS2 u1 u2) : + Id (squareS2 a0 a2 (compN a0 q0 u0) (compN a2 q2 u2) (compId S2 a0 a1 a2 p0 p1)) + (vComp a0 a1 a2 (compN a0 q0 u0) (compN a1 q1 u1) (compN a2 q2 u2) p0 p1 + (hComp a0 a1 q0 q1 p0 u0 u1 s t) + (hComp a1 a2 q1 q2 p1 u1 u2 s1 t1)) + (hComp a0 a2 q0 q2 (compId S2 a0 a1 a2 p0 p1) u0 u2 + (vComp a0 a1 a2 q0 q1 q2 p0 p1 s s1) + (vComp north north north u0 u1 u2 r2 r2 t t1)) = + transport + ( Id (squareS2 (q0@i) (q2@i) (compN (q0@i) (q0@i/\j) u0) (compN (q2@i) (q2@i/\j) u2) (compId S2 (q0@i) (q1@i) (q2@i) (s@i@k) (s1@i@k))) + (vComp (q0@i) (q1@i) (q2@i) (compN (q0@i) (q0@i/\j) u0) (compN (q1@i) (q1@i/\j) u1) (compN (q2@i) (q2@i/\j) u2) (s@i@k) (s1@i@k) + (hComp (q0@i) (q1@i) (q0@i/\j) (q1@i/\j) (s@i@k) u0 u1 (s@i/\j@k) t) + (hComp (q1@i) (q2@i) (q1@i/\j) (q2@i/\j) (s1@i@k) u1 u2 (s1@i/\j@k) t1)) + (hComp (q0@i) (q2@i) (q0@i/\j) (q2@i/\j) (compId S2 (q0@i) (q1@i) (q2@i) (s@i@k) (s1@i@k)) u0 u2 + (vComp (q0@i) (q1@i) (q2@i) (q0@i/\j) (q1@i/\j) (q2@i/\j) (s@i@k) (s1@i@k) (s@i/\j@k) (s1@i/\j@k)) + (vComp north north north u0 u1 u2 r2 r2 t t1))) + (refl (sqS2 u0 u2) (vComp north north north u0 u1 u2 r2 r2 t t1)) + +corExLem (t t1 s s1 : Omega2) : + Id Omega2 (vcomp (hcomp t s) (hcomp t1 s1)) (hcomp (vcomp t t1) (vcomp s s1)) = + exLem north north north r2 r2 r2 r2 r2 r2 r2 r2 s s1 t t1 + +-- we should be able to deduce that vcomp t s = hcomp t s + +rR2 : Omega2 = refl loopS2 r2 + +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 = + transport (Id (Id A a (p@i)) (compId A a a (p@i) (refl A a) (p@i/\j)) (p@i/\j)) + (refl (Id A a a) (refl A a)) + +lemRV (s:Omega2) : Id Omega2 (vcomp rR2 s) s = lemIdl S2 north north (s@i)@k@j + +lemRH (s:Omega2) : Id Omega2 (hcomp rR2 s) s = lemIdl S2 north north (s@l@j)@k@i + +lem1 (s t:Omega2) : Id Omega2 (vcomp t s) (hcomp t s) = + compId Omega2 (vcomp t s) (hcomp t (vcomp rR2 s)) (hcomp t s) + (compId Omega2 (vcomp t s) (vcomp (hcomp t rR2) (hcomp rR2 s)) (hcomp t (vcomp rR2 s)) rem1 rem2) + rem3 + where + rem1 : Id Omega2 (vcomp t s) (vcomp (hcomp t rR2) (hcomp rR2 s)) = vcomp t (lemRH s@-i) + rem2 : Id Omega2 (vcomp (hcomp t rR2) (hcomp rR2 s)) (hcomp t (vcomp rR2 s)) = corExLem t rR2 rR2 s + rem3 : Id Omega2 (hcomp t (vcomp rR2 s)) (hcomp t s) = hcomp t (lemRV s@i) + +lemInv (A:U) (a b:A) (p:Id A a b) : Id (Id A a a) (compId A a b a p (p@-i)) (refl A a) = + transport (Id (Id A a a) (compId A a (p@i) a (p@i/\j) (p@i/\-j)) (refl A a)) (refl (Id A a a) (refl A a)) + +g2 : Omega2 = test1 +invG2 : Omega2 = g2@i@-j + +-- lem2 : Id Omega2 (hcomp g2 invG2) rR2 = lemInv S2 north north (g2@l@j)@k@i + +lem3 : Id Omega2 (vcomp g2 invG2) rR2 = lemInv S2 north north (g2@i)@k@j +-- compId Omega2 (vcomp g2 invG2) (hcomp h2 invG2) rR2 (lem1 g2 invG2) lem2 + +lemInv1 (A:U) (a b:A) (p:Id A a b) : Id (Id A b b) (compId A b a b (p@-i) p) (refl A b) = + transport (Id (Id A b b) (compId A b (p@-i) b (p@-i\/-j) (p@-i\/j)) (refl A b)) (refl (Id A b b) (refl A b)) + +lem4 : Id Omega2 (vcomp invG2 g2) rR2 = lemInv1 S2 north north (g2@i)@k@j + +-- commutativity + +lem5 (s t:Omega2) : Id Omega2 (vcomp t s) (vcomp s t) = + compId Omega2 (vcomp t s) (vcomp (hcomp rR2 s) t) (vcomp s t) + (compId Omega2 (vcomp t s) (hcomp (vcomp rR2 t) s) (vcomp (hcomp rR2 s) t) + (compId Omega2 (vcomp t s) (hcomp t s) (hcomp (vcomp rR2 t) s) (lem1 s t) rem4) + rem5) + rem6 + where + rem4 : Id Omega2 (hcomp t s) (hcomp (vcomp rR2 t) s) = hcomp (lemRV t@-i) s + rem5 : Id Omega2 (hcomp (vcomp rR2 t) s) (vcomp (hcomp rR2 s) t) = corExLem rR2 t s rR2@-i + rem6 : Id Omega2 (vcomp (hcomp rR2 s) t) (vcomp s t) = vcomp (lemRH s@i) t + +genPi3S2 : Id Omega2 rR2 rR2 = + compId Omega2 rR2 (vcomp invG2 g2) rR2 (compId Omega2 rR2 (vcomp g2 invG2) (vcomp invG2 g2) rem1 rem2) lem4 + where + rem1 : Id Omega2 rR2 (vcomp g2 invG2) = lem3@-i + rem2 : Id Omega2 (vcomp g2 invG2) (vcomp invG2 g2) = lem5 invG2 g2 + + diff --git a/examples/pi1s2.ctt b/examples/pi1s2.ctt index 5eefc4b..8ac4394 100644 --- 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 9b17e30..82b1d85 100644 --- 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 5d219ce..20a80c9 100644 --- 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) test2S : Z = windingS loop2S + +-- The sphere is the suspension of the circle: +S2 : U = susp S1 + +loopS2 : U = Id S2 north north diff --git a/examples/truncS2.ctt b/examples/truncS2.ctt index e1003e2..b6a1aa4 100644 --- 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 (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) = (u:X) * (v:X) * (lemS1Set (Id X u v) (gX u v) @ i) -- 2.34.1