{- | The generalized Blakers-Massey theorem.
- The proof combines ideas from the following papers:
- * Kuen-Bang Hou (Favonia), Eric Finster, Dan Licata, Peter LeFanu Lumsdaine, A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory (https://arxiv.org/abs/1605.03227, https://github.com/HoTT/HoTT-Agda/blob/master/theorems/homotopy/BlakersMassey.agda)
- * Mathieu Anel, Georg Biedermann, Eric Finster, André Joyal, A Generalized Blakers-Massey Theorem (https://arxiv.org/abs/1703.09050)
- -}
\import Equiv
\import Equiv.Sigma
\import Equiv.Univalence
\import HLevel
\import Homotopy.Fibration
\import Homotopy.Join
\import Homotopy.Localization.Connected
\import Homotopy.Localization.Universe
\import Homotopy.Pushout
\import Logic
\import Paths
\import Paths.Meta
\lemma genBlakersMassey {d : Data} (x0 : X) (y0 : Y) : isConnectedMap (pbMap {d} {x0} {y0})
=> \lam p => surjective (POData.pullback_pushout-surjective {\new POData Y X (\lam y x => Q x y)} y0 x0 (inv (pmap swap p))) p
\where {
\open Localization
-- | It is easier to prove the theorem if the type ``\Sigma (y : Y) (Q x0 y)`` is inhabited.
\lemma surjective {d : Data} {x0 : X} {y0 : Y} (q : TruncP (\Sigma (y : Y) (Q x0 y))) : isConnectedMap (pbMap {d} {x0} {y0}) \elim q
| inP (y,q0) => \lam p => contr=>isConnected (Fib pbMap p) (DataExt.code-contr {\new DataExt { | Data => d | x0 => x0 | y0 => y | q0 => q0 }} p)
\class EquivData \noclassifying (A B : \hType) \extends ReflUniverse {
| M : A -> Connected
| N : B -> Connected
| f : \Sigma (a : A) (M a) -> \Sigma (b : B) (N b)
| g : \Sigma (b : B) (N b) -> \Sigma (a : A) (M a)
| p : \Pi (a : A) (m : M a) -> (g (f (a,m))).1 = a
| q : \Pi (b : B) (n : N b) -> (f (g (b,n))).1 = b
\func eval (a : A) (m : M a) : lift (\lam a => sec {Connected.equiv {M a} (LType B)} (\lam m => lEta (f (a,m)).1)) (lEta a) = lEta (f (a,m)).1 =>
lift-prop (\lam a => sec {Connected.equiv {M a} (LType B)} (\lam m => lEta (f (a,m)).1)) a *> path (\lam i => (f_sec {Connected.equiv {M a} (LType B)} (\lam m => lEta (f (a,m)).1) @ i) m)
\lemma equiv-lemma : Equiv {LType A} {LType B} (lift (\lam a => sec {Connected.equiv {M a} (LType B)} (\lam m => lEta (f (a,m)).1)))
=> \let | E1 a => Connected.equiv {M a} (LType B)
| E2 b => Connected.equiv {N b} (LType A)
| f1 a m => lEta (f (a,m)).1
| g1 b n => lEta (g (b,n)).1
| F a => sec {E1 a} (f1 a)
| G b => sec {E2 b} (g1 b)
\in localization-equiv F G
(\lam a => sec {Connected.equiv {M a} (pathLocal (lift G (F a)) (lEta a))}
(\lam m => lift G (F a) ==< path (\lam i => lift G ((f_sec {E1 a} (f1 a) @ i) m)) >==
lift G (f1 a m) ==< lift-prop G (f (a,m)).1 >==
G (f (a,m)).1 ==< path (\lam i => (f_sec {E2 (f (a,m)).1} (g1 (f (a,m)).1) @ i) (f (a,m)).2) >==
inL (g (f (a,m))).1 ==< pmap inL (p a m) >==
inL a `qed))
(\lam b => sec {Connected.equiv {N b} (pathLocal (lift F (G b)) (lEta b))}
(\lam n => lift F (G b) ==< path (\lam i => lift F ((f_sec {E2 b} (g1 b) @ i) n)) >==
lift F (g1 b n) ==< lift-prop F (g (b,n)).1 >==
F (g (b,n)).1 ==< path (\lam i => (f_sec {E1 (g (b,n)).1} (f1 (g (b,n)).1) @ i) (g (b,n)).2) >==
inL (f (g (b,n))).1 ==< pmap inL (q b n) >==
inL b `qed))
}
\class POData {
| X : \hType
| Y : \hType
| Q : X -> Y -> \hType
\func PO => PushoutData {\Sigma (x : X) (y : Y) (Q x y)} __.1 __.2
\func swap (x : PO) : PushoutData {\Sigma (y : Y) (x : X) (Q x y)} __.1 __.2
| pinl b => pinr b
| pinr c => pinl c
| pglue (x,y,q) i => pglue (y,x,q) (inv (path (\lam j => j)) @ i)
\func pbMap {x : X} {y : Y} (q : Q x y) : pinl x = {PO} pinr y => PushoutData.ppglue ((x,y,q) : \Sigma (x : X) (y : Y) (Q x y))
\lemma pullback_pushout-surjective (x : X) (y : Y) (p : pinl x = {PO} pinr y) : TruncP (\Sigma (x' : X) (Q x' y))
=> \have | EP => \new EmbeddingPushout {
| A => \Sigma (y : Y) (TruncP (\Sigma (x : X) (Q x y)))
| B => PushoutData {\Sigma (x : X) (y : Y) (Q x y)} {X} {\Sigma (y : Y) (TruncP (\Sigma (x : X) (Q x y)))} __.1 (\lam p => (p.2, inP (p.1,p.3)))
| C => Y
| f => pinr
| g => Embedding.projection (\lam y => TruncP (\Sigma (x : X) (Q x y)))
}
| t => ret {EP.pullback-path-equiv (pinl x) y} (pmap
(\case __ \with {
| pinl x => pinl (pinl x)
| pinr y => pinr y
| pglue (x,y,q) i =>
(pmap pinl (PushoutData.ppglue {\Sigma (x : X) (y : Y) (Q x y)} (x,y,q)) *>
PushoutData.ppglue {EP.A} (y, inP (x,q))) @ i
}) p)
\in rewrite t.3 t.1.2
}
\open POData
\class Data \extends ReflUniverse, POData
| ch {x x' : X} {y y' : Y} (q0 : Q x y) (q1 : Q x y') (q2 : Q x' y)
: isConnectedType (Join (\Sigma (p : y = y') (transport (Q x) p q0 = q1)) (\Sigma (p : x = x') (transport (`Q y) p q0 = q2)))
\class DataExt \extends Data {
| x0 : X
| y0 : Y
| q0 : Q x0 y0
\func code-left {x : X} {w : PO} (p : pinl x = {PO} w) (p' : pinl x0 = w) : \hType
=> LType (\Sigma (q1 : Q x y0) (pbMap q0 *> inv (pbMap q1) *> p = p'))
\func code-glue-gen {x : X} {w : PO} (code : pinl x0 = w -> \hType) (p : pinl x = w)
(t : \Pi (p' : pinl x0 = w) -> Equiv {code-left p p'} {code p'})
: transport (pinl x0 = __ -> \hType) p (code-left idp) = code \elim p
| idp => path (\lam i p' => Equiv-to-= (t p') @ i)
\func code-glue {x : X} {y : Y} (q : Q x y)
: transport (pinl x0 = __ -> \hType) (pbMap q) (code-left idp) = (\lam p => LType (Fib pbMap p))
=> code-glue-gen (\lam p => LType (Fib pbMap p)) (pbMap q) (code.equiv q)
\func code {w : PO} (p : pinl x0 = w) : \hType \elim w
| pinl x => code-left idp p
| pinr y => LType (Fib pbMap p)
| pglue (x,y,q) i => (pathOver (code-glue q) @ i) p
\where {
\func equivData {x : X} {y : Y} (q : Q x y) (p : pinl x0 = {PO} pinr y) : EquivData \cowith
| isLocal => isLocal
| localization => localization
| A => \Sigma (q1 : Q x y0) (pbMap q0 *> inv (pbMap q1) *> pbMap q = p)
| B => Fib pbMap p
| M a => \new Connected {
| X => Join (\Sigma (p : y0 = y) (transport (Q x) p a.1 = q)) (\Sigma (p : x = x0) (transport (`Q y0) p a.1 = q0))
| connected => ch a.1 q q0
}
| N b => \new Connected {
| X => Join (\Sigma (p : y = y0) (transport (Q x0) p b.1 = q0)) (\Sigma (p : x0 = x) (transport (`Q y) p b.1 = q))
| connected => ch b.1 q0 q
}
| f ad => LR q p ad.1 ad.2
| g bd => RL q0 q p bd.1 bd.2
| p => LRL q p
| q => RLR q p
\lemma equiv {x : X} {y : Y} (q : Q x y) (p : pinl x0 = {PO} pinr y) => EquivData.equiv-lemma {equivData q p}
\func pathLem1 {A : \hType} {a a' a'' : A} (p : a = a') (q : a'' = a') : p *> inv q *> q = p
| idp, idp => idp
\func pathLem2-gen {A : \hType} {a a' a'' : A} {p1 p2 : a = a'} {q : a = a''} (t : p1 *> inv p2 = idp) : p1 *> inv p2 *> q = q \elim q
| idp => t
\func pathLem2 {A : \hType} {a a' a'' : A} (p : a = a') (q : a = a'') : p *> inv p *> q = q
=> pathLem2-gen (*>_inv p)
\func pathLem3 {A : \hType} {a a' : A} (p : a = a') : pathLem1 p p = pathLem2 p p
| idp => idp
\func LR {x : X} {y : Y} (q : Q x y) (p : pinl x0 = {PO} pinr y)
(a : \Sigma (q1 : Q x y0) (pbMap q0 *> inv (pbMap q1) *> pbMap q = p))
(m : Join (\Sigma (p : y0 = y) (transport (Q x) p a.1 = q)) (\Sigma (p : x = x0) (transport (`Q y0) p a.1 = q0)))
: \Sigma (b : Fib pbMap p) (Join (\Sigma (p : y = y0) (transport (Q x0) p b.1 = q0)) (\Sigma (p : x0 = x) (transport (`Q y) p b.1 = q)))
\elim a, m
| (a1,a2), jinl (idp,idp) => ((q0, inv (pathLem1 (pbMap q0) (pbMap a1)) *> a2), pinl (idp,idp))
| (a1,a2), jinr (idp,idp) => ((q, inv (pathLem2 (pbMap a1) (pbMap q)) *> a2), pinr (idp,idp))
| (a1,a2), pglue ((idp,idp),(idp,idp)) i => ((q0, inv (pathLem3 (pbMap q0) @ i) *> a2), pglue ((idp,idp),(idp,idp)) i)
\func RL {x : X} {y : Y} (q0 : Q x0 y0) (q : Q x y) (p : pinl x0 = {PO} pinr y)
(b : \Sigma (q2 : Q x0 y) (pbMap q2 = p))
(n : Join (\Sigma (p : y = y0) (transport (Q x0) p b.1 = q0)) (\Sigma (p : x0 = x) (transport (`Q y) p b.1 = q)))
: \Sigma (a : \Sigma (q1 : Q x y0) (pbMap q0 *> inv (pbMap q1) *> pbMap q = p))
(Join (\Sigma (p : y0 = y) (transport (Q x) p a.1 = q)) (\Sigma (p : x = x0) (transport (`Q y0) p a.1 = q0)))
\elim n
| jinl (idp,idp) => ((q, pathLem1 (pbMap b.1) (pbMap q) *> b.2), pinl (idp,idp))
| jinr (idp,idp) => ((q0, pathLem2 (pbMap q0) (pbMap b.1) *> b.2), pinr (idp,idp))
| pglue ((idp,idp),(idp,idp)) i => ((b.1, (pathLem3 (pbMap b.1) @ i) *> b.2), pglue ((idp,idp),(idp,idp)) i)
\func LRL {x : X} {y : Y} (q : Q x y) (p : pinl x0 = {PO} pinr y)
(a : \Sigma (q1 : Q x y0) (pbMap q0 *> inv (pbMap q1) *> pbMap q = p))
(m : Join (\Sigma (p : y0 = y) (transport (Q x) p a.1 = q)) (\Sigma (p : x = x0) (transport (`Q y0) p a.1 = q0)))
: (RL q0 q p (LR q p a m).1 (LR q p a m).2).1 = a
\elim a, m
| (a1,idp), jinl (idp,idp) => path (\lam i => (q, *>_inv (pathLem1 (pbMap q0) (pbMap q)) @ i))
| (a1,idp), jinr (idp,idp) => path (\lam i => (q0, *>_inv (pathLem2 (pbMap q0) (pbMap q)) @ i))
| (a1,idp), pglue ((idp,idp),(idp,idp)) j => path (\lam i => (q0, *>_inv (pathLem3 (pbMap q0) @ j) @ i))
\func RLR {x : X} {y : Y} (q : Q x y) (p : pinl x0 = {PO} pinr y)
(b : \Sigma (q2 : Q x0 y) (pbMap q2 = p))
(n : Join (\Sigma (p : y = y0) (transport (Q x0) p b.1 = q0)) (\Sigma (p : x0 = x) (transport (`Q y) p b.1 = q)))
: (LR q p (RL q0 q p b n).1 (RL q0 q p b n).2).1 = b
\elim b, n
| (b1,idp), jinl (idp,idp) => path (\lam i => (q0, inv_*> (pathLem1 (pbMap q0) (pbMap q)) @ i))
| (b1,idp), jinr (idp,idp) => path (\lam i => (q, inv_*> (pathLem2 (pbMap q0) (pbMap q)) @ i))
| (b1,idp), pglue ((idp,idp),(idp,idp)) j => path (\lam i => (q0, inv_*> (pathLem3 (pbMap q0) @ j) @ i))
}
\func coerce-path-gen {w : PO} (p : pinl x0 = w) (t : transport (pinl x0 = __ -> \hType) p (code-left idp) = code)
: code-left idp idp = code p \elim p
| idp => path ((t @ __) idp)
\func coerce-path {w : PO} (p : pinl x0 = w)
: code-left idp idp = code p
=> coerce-path-gen p (pmapd (\lam _ => code) p)
\func Left {w : PO} (p : pinl x0 = w) => \Sigma (q : Q x0 y0) (pbMap q0 *> inv (pbMap q) *> p = p)
\func code-left-diag {w : PO} (p : pinl x0 = w) (v : code-left idp idp) : code-left p p
=> lmap {_} {Left idp} {Left p} (\lam t => (t.1, code.pathLem2-gen t.2)) v
\func coerce-path-glue-gen {w : PO} (p : pinl x0 = w) (t : \Pi (p' : pinl x0 = w) -> Equiv {code-left p p'} {code p'}) (v : code-left idp idp)
: transport (\lam T => T) (coerce-path-gen p (code-glue-gen code p t)) v = t p (code-left-diag p v) \elim p
| idp => pmap (t idp) (inv (lmap.id-prop v))
\func code-center {w : PO} (p : pinl x0 = w) : code p
=> transport (\lam T => T) (coerce-path p) (lEta point)
\where \func point : Left idp => (q0, *>_inv (pbMap q0))
\func code-path (p : pinl x0 = {PO} pinr y0) (c : Fib pbMap p) : code-center p = lEta c \elim c
| (q,idp) =>
code-center (pbMap q)
==< pmap (\lam s => transport (\lam T => T) (coerce-path-gen (pbMap q) s) (lEta code-center.point)) (pmapd_pathOver (pinl x0 = __ -> \hType) (\lam _ => code) (pbMap q) (code-glue q) idp) >==
transport (\lam T => T) (coerce-path-gen (pbMap q) (code-glue q)) (lEta code-center.point)
==< coerce-path-glue-gen (pbMap q) (code.equiv q) (lEta code-center.point) >==
code.equiv q (pbMap q) (code-left-diag (pbMap q) (lEta code-center.point))
==< pmap (code.equiv q (pbMap q)) (lift-prop (\lam (t : Left idp) => inL ((t.1, code.pathLem2-gen t.2) : Left (pbMap q))) code-center.point) >==
code.equiv q (pbMap q) (lEta ((q0, code.pathLem2 (pbMap q0) (pbMap q)) : Left (pbMap q)))
==< EquivData.eval {code.equivData q (pbMap q)} (q0, code.pathLem2 (pbMap q0) (pbMap q)) (pinr (idp,idp)) >==
lEta ((q, inv (code.pathLem2 (pbMap q0) (pbMap q)) *> code.pathLem2 (pbMap q0) (pbMap q)) : Fib pbMap p)
==< pmap (\lam x => lEta ((q,x) : Fib pbMap p)) (inv_*> (code.pathLem2 (pbMap q0) (pbMap q))) >==
lEta ((q, idp) : Fib pbMap p)
`qed
\lemma code-contr {w : PO} (p : pinl x0 = w) : Contr (code p) \cowith
| center => code-center p
| contraction => transport (\lam t => \Pi (c : code t.2) -> code-center t.2 = c) (isContr=>isProp (lsigma {PO} (pinl x0)) (pinr y0, pbMap q0) (w, p))
(\lam c => remove_inL (\lam _ => code-center (pbMap q0)) (\lam c => c) (code-path (pbMap q0)) c)
}
}