From d74ce0731763d99c173367d1fabdc9e9a37204b3 Mon Sep 17 00:00:00 2001 From: coquand Date: Thu, 30 Apr 2015 13:44:38 +0200 Subject: [PATCH] piS2 is trivial --- examples/deppath.ctt | 15 +++++++ examples/pi1S2.ctt | 49 ++++++++-------------- examples/thm7312.ctt | 96 ++++++++++++++++++++++++++++++++++++++++++++ examples/truncS2.ctt | 63 ++++++++++++++++++++++++++++- 4 files changed, 189 insertions(+), 34 deletions(-) create mode 100644 examples/deppath.ctt create mode 100644 examples/thm7312.ctt diff --git a/examples/deppath.ctt b/examples/deppath.ctt new file mode 100644 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) = + IdP ( p @ (i\/l)) (transport ( p @ (i/\l)) u0) u1 + +funDepTrInv (A0 A1 :U) (p:Id U A0 A1) (u0:A0) (u1:A1) : + Id U (Id A0 u0 (transport (p@-i) u1)) (IdP p u0 u1) = + IdP ( p @ (i/\l)) u0 (transport ( p @ (i\/-l)) u1) + +funDep (A0 A1 :U) (p:Id U A0 A1) (u0:A0) (u1:A1) : + Id U (Id A0 u0 (transport (p@-i) u1)) (Id A1 (transport p u0) u1) = + Id (p @ i) (transport ( p @ (i/\l)) u0) (transport ( p @ (i\/-l)) u1) \ No newline at end of file diff --git a/examples/pi1S2.ctt b/examples/pi1S2.ctt index 9c3c0a0..e79d97b 100644 --- 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 (Id (p@-i) (transport (p@(-i/\j)) a0) (transport (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 = merid{S2} base@i -corr2 (x:gTrunc S2) : Id (gTrunc S2) x (inc north) = corr1@i x +trivS2 : pi1S2 = inc (refl S2 north) +loopS2 : pi1S2 = inc (compId S2 north south north meridS2 (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) = - inc (comp S2 north - [ (i = 0) -> comp S2 south - [ (j = 0) -> comp S2 north - [ (k = 0) -> comp S2 south - [ (l = 0) -> comp S2 north - [ (m = 0) -> comp S2 south - [ (n = 0) ->

comp S2 north - [ (p = 0) -> comp S2 north [ (q = 1) -> merid {S2} base @ r ] ] ] ] ] ] ] ]) +eqS1 +eqS2 : Id U S2 stwo = subst U susp S1 sone (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 ((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 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) -> 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 6349b8c..e1003e2 100644 --- 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 (Id (p@-i) (transport (p@(-i/\j)) a0) (transport (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) = corr1@i x + +propgTruncS2 : prop (gTrunc S2) = + \ (x y : gTrunc S2) -> compId (gTrunc S2) x (inc north) y (corr2 x) (corr2 y@-i) + + +test : Id (gTrunc S2) (inc south) (inc north) = corr2 (inc south) + +-- normal form + +test : Id (gTrunc S2) (inc south) (inc north) = + inc (comp S2 north + [ (i = 0) -> comp S2 south + [ (j = 0) -> comp S2 north + [ (k = 0) -> comp S2 south + [ (l = 0) -> comp S2 north + [ (m = 0) -> comp S2 south + [ (n = 0) ->

comp S2 north + [ (p = 0) -> comp S2 north [ (q = 1) -> 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) (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 ((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) = + inc (comp stwo north + [ (i = 0) -> comp stwo south + [ (j = 0) -> comp stwo north + [ (k = 0) -> comp stwo south + [ (l = 0) -> comp stwo north + [ (m = 0) -> comp stwo south + [ (n = 0) ->

comp stwo north + [ (p = 0) -> comp stwo north + [ (q = 1) -> merid {stwo} north @ r ] ] ] ] ] ] ] ]) -- 2.34.1