\import Equiv
\import Equiv.Univalence
\import Function
\import HLevel
\import Homotopy.Cube
\import Homotopy.Pushout
\import Homotopy.Sphere
\import Homotopy.Suspension
\import Logic
\import Paths
\func Join (A B : \Type) => PushoutData {\Sigma A B} __.1 __.2
\where {
\use \level levelProp {A B : \Prop} : isProp (Join A B) => isContr'=>isProp {Join A B} (\case __ \with {
| pinl a => transport (Contr __) (QEquiv-to-= (Join-sym B A)) (Join_Contr B (isProp=>isContr prop-isProp a))
| pinr b => Join_Contr A (isProp=>isContr prop-isProp b)
})
\lemma from-|| {A B : \Prop} (x : A || B) : Join A B \elim x
| byLeft a => jinl a
| byRight b => jinr b
}
\cons jinl {A B : \Type} (a : A) : Join A B => pinl a
\cons jinr {A B : \Type} (b : B) : Join A B => pinr b
\func jglue {A B : \Type} (a : A) (b : B) : jinl a = jinr b => path (pglue (a,b))
\lemma Join_Contr (A : \Type) (B : Contr) : Contr (Join A B) \cowith
| center => jinr B.center
| contraction x => \case \elim x \with {
| jinl a => inv (jglue a B.center)
| jinr b => pmap jinr (B.contraction b)
| pglue (a,b) => Cube2.map
(inv (jglue a B.center))
(pmap jinr (B.contraction b))
(idpe (jinr B.center))
(jglue a b)
(Jl (\lam x p => inv (jglue a B.center) = pmap jinr p *> inv (jglue a x)) (inv (idp_*> _)) (B.contraction b))
}
\func Join_Sphere0 (A : \Type) : QEquiv {Join (Sphere 0) A} {Susp A} \cowith
| f => joinSusp
| ret => suspJoin
| ret_f => joinSuspJoin
| f_sec => suspJoinSusp
\where {
\func joinSusp {A : \Type} (j : Join (Sphere 0) A) : Susp A
| jinl north => north
| jinl south => south
| jinl (pglue () _)
| jinr _ => south
| pglue (north, a) i => pglue a i
| pglue (south, _) _ => south
| pglue (pglue () _, _) _
\func suspJoin {A : \Type} (s : Susp A) : Join (Sphere 0) A
| north => jinl north
| south => jinl south
| pglue a => jglue north a *> inv (jglue south a)
\func joinSuspJoin {A : \Type} (j : Join (Sphere 0) A) : suspJoin (joinSusp j) = j
| jinl north => idp
| jinl south => idp
| jinl (pglue () _)
| jinr a => jglue south a
| pglue (north, a) j => path (Cube2.map
(jglue north a *> inv (jglue south a))
(jglue north a)
(idpe (jinl north))
(jglue south a)
idp @ __ @ j)
| pglue (south, a) j => path (\lam i => pglue (south,a) (I.squeeze i j))
| pglue (pglue () _, _) _
\func suspJoinSusp {A : \Type} (s : Susp A) : joinSusp (suspJoin s) = s
| north => idp
| south => idp
| pglue a i =>
\have t =>
pmap joinSusp (jglue north a *> inv (jglue south a)) ==< pmap_*>-comm joinSusp (jglue north a) (inv (jglue south a)) >==
pmerid a *> pmap joinSusp (inv (jglue south a)) ==< pmap (pmerid a *>) (pmap_inv-comm joinSusp (jglue south a)) >==
pmerid a `qed
\in path (t @ __ @ i)
}
\func Join-sym (A B : \Type) : QEquiv {Join A B} {Join B A} \cowith
| f => flip
| ret => flip
| ret_f => flip-flip
| f_sec => flip-flip
\where {
\func flip {A B : \Type} (j : Join A B) : Join B A
| jinl a => jinr a
| jinr b => jinl b
| pglue (a,b) => inv (jglue b a)
\func flip-flip {A B : \Type} (j : Join A B) : flip (flip j) = j
| jinl a => idp
| jinr b => idp
| pglue (a,b) i =>
\have p => pmap_inv-comm flip (jglue b a) *> inv_inv (jglue a b)
\in path (p @ __ @ i)
}
\func Join-assoc (A B C : \Type) : QEquiv {Join (Join A B) C} {Join A (Join B C)} \cowith
| f => leftToRight
| ret => rightToLeft
| ret_f => leftRightLeft
| f_sec => rightLeftRight
\where {
\open I
\func leftToRight {A B C : \Type} (j : Join (Join A B) C) : Join A (Join B C)
| jinl (jinl a) => jinl a
| jinl (jinr b) => jinr (jinl b)
| jinl (pglue (a,b) j) => pglue (a, jinl b) j
| jinr c => jinr (jinr c)
| pglue (jinl a, c) i => pglue (a, jinr c) i
| pglue (jinr b, c) i => jinr (pglue (b,c) i)
| pglue (pglue (a,b), c) =>
Jl.def (\lam x p => Cube2 (jglue a x) (pmap jinr p) (jglue a (jinl b)) (idpe (jinr x)))
(path (\lam j => path (\lam i => pglue (a, jinl b) (squeezeR j i))))
(jglue b c)
\func rightToLeft {A B C : \Type} (j : Join A (Join B C)) : Join (Join A B) C
| jinl a => jinl (jinl a)
| jinr (jinl b) => jinl (jinr b)
| jinr (jinr c) => jinr c
| jinr (pglue (b,c) j) => pglue (jinr b, c) j
| pglue (a, jinl b) i => jinl (pglue (a,b) i)
| pglue (a, jinr c) i => pglue (jinl a, c) i
| pglue (a, pglue (b,c)) =>
Jl.def (\lam x p => Cube2 (pmap jinl p) (jglue (jinl a) c) (idpe (jinl (jinl a))) (jglue x c))
(path (\lam j => path (\lam i => pglue (jinl a, c) (squeeze j i))))
(jglue a b)
\func leftRightLeft {A B C : \Type} (j : Join (Join A B) C) : rightToLeft (leftToRight j) = j
| jinl (jinl a) => idp
| jinl (jinr b) => idp
| jinl (pglue (a,b) j) => idp
| jinr c => idp
| pglue (jinl a, c) i => idp
| pglue (jinr b, c) i => idp
| pglue (pglue (a,b) j, c) i =>
\let | s1 {y} (q : jinl b = y) : Cube2 (pmap rightToLeft (jglue a y))
(pmap (\lam t => rightToLeft (jinr t)) q)
(pmap jinl (jglue a b))
(idpe (rightToLeft (jinr y)))
=> path (\lam j => path (\lam i =>
rightToLeft (Jl.def (\lam x p => Cube2 (jglue a x) (pmap jinr p) (jglue a (jinl b)) (idpe (jinr x)))
(path (\lam j => path (\lam i => pglue (a, jinl b) (squeezeR j i))))
q @ j @ i)))
| s2 {y} (q : jinl b = y) =>
Jl.def (\lam x p => Cube2 (pmap rightToLeft (jglue a x))
(pmap (\lam t => rightToLeft (jinr t)) p)
(pmap jinl (jglue a b))
(idpe (rightToLeft (jinr x))))
(path (\lam j => path (\lam i => jinl (pglue (a,b) (squeezeR j i)))))
q
| proof => coe (\lam n =>
coe (\lam k => Cube2 (coe (\lam l => Cube2 (path (\lam m => jinl (pglue (a,b) (squeeze (squeeze l m) n))))
(jglue (jinl a) c)
(idpe (jinl (jinl a)))
(jglue (pglue (a,b) (squeeze l n)) c))
(path (\lam j => path (\lam i => pglue (jinl a, c) (squeeze j i))))
right @ k)
(path (\lam j => pglue (pglue (a,b) n, c) (squeeze k j)))
(path (\lam m => jinl (pglue (a,b) (squeeze m n))))
(idpe (pglue (pglue (a,b) n, c) k)))
(path (\lam j => path (\lam i => jinl (pglue (a,b) (squeeze (squeezeR j i) n)))))
right
= path (\lam j => path (pglue (pglue (a,b) (squeeze j n), c)))
) (Jl (\lam y q => Jl.def (\lam x p => Cube2 p p idp idp) idp q = idp) idp (jglue (jinl a) c)) right
\in path ((Jl (\lam y q => s1 q = s2 q) idp (jglue b c) *> proof) @ __ @ j @ i)
\func rightLeftRight {A B C : \Type} (j : Join A (Join B C)) : leftToRight (rightToLeft j) = j
| jinl a => idp
| jinr (jinl b) => idp
| jinr (jinr c) => idp
| jinr (pglue (b,c) j) => idp
| pglue (a, jinl b) i => idp
| pglue (a, jinr c) i => idp
| pglue (a, pglue (b,c) j) i =>
\let | s1 {y} (q : jinl a = y) : Cube2 (pmap (\lam t => leftToRight (jinl t)) q)
(jglue a (jinr c))
(idpe (jinl a))
(pmap leftToRight (jglue y c))
=> path (\lam j => path (\lam i =>
leftToRight (Jl.def (\lam x p => Cube2 (pmap jinl p) (jglue (jinl a) c) (idpe (jinl (jinl a))) (jglue x c))
(path (\lam i => path (\lam j => pglue (jinl a, c) (squeeze i j))))
q
@ j @ i)))
| s2 {y} (q : jinl a = y) =>
Jl.def (\lam x p => Cube2 (pmap (\lam t => leftToRight (jinl t)) p) (jglue a (jinr c)) (idpe (jinl a)) (pmap leftToRight (jglue x c)))
(path (\lam j => path (\lam i => pglue (a, jinr c) (squeeze j i))))
q
| proof =>
Jl (\lam y q => coe (\lam k => Cube2 (path (\lam i => pglue (a, jinl b) (squeeze k i)))
(jglue a y)
(idpe (jinl a))
(Jl.def (\lam x p => Cube2 (jglue a x) (pmap jinr p) (jglue a (jinl b)) (idpe (jinr x)))
(path (\lam j => path (\lam i => pglue (a, jinl b) (squeezeR j i))))
q
@ k))
(path (\lam j => path (\lam i => pglue (a,y) (squeeze j i))))
right
= path (\lam j => path (pglue (a, q @ j))))
(Jl (\lam y q => coe (\lam k => Cube2 (path (q @ squeeze k __))
q
(idpe (jinl a))
(path (q @ squeezeR k __)))
(path (\lam j => path (q @ squeeze j __)))
right
= idpe q)
idp
(jglue a (jinl b)))
(jglue b c)
\in path ((Jl (\lam y q => s1 q = s2 q) idp (jglue a b) *> proof) @ __ @ j @ i)
}
\func Join_Susp (A B : \Type) : Join (Susp A) B = Susp (Join A B) =>
Join (Susp A) B ==< pmap (`Join B) (QEquiv-to-= (symQEquiv (Join_Sphere0 A))) >==
Join (Join (Sphere 0) A) B ==< QEquiv-to-= (Join-assoc (Sphere 0) A B) >==
Join (Sphere 0) (Join A B) ==< QEquiv-to-= (Join_Sphere0 (Join A B)) >==
Susp (Join A B) `qed
\func Join_Sphere (A : \Type) (n : Nat) : Join (Sphere n) A = iterr Susp (suc n) A \elim n
| 0 => QEquiv-to-= (Join_Sphere0 A)
| suc n => Join_Susp (Sphere n) A *> pmap Susp (Join_Sphere A n)