open import 1Lab.Prelude

open import Data.Bool

open import Homotopy.Space.Suspension
open import Homotopy.Pushout

module Homotopy.Join where

The join of typesπŸ”—

private variable
  β„“ β„“' : Level
  A B C X Y Z : Type β„“

The join of two types and written is the pushout under the diagram 

_βˆ—_ : Type β„“ β†’ Type β„“' β†’ Type (β„“ βŠ” β„“')
A βˆ— B = Pushout (A Γ— B) fst snd

infixr 30 _βˆ—_

pattern join x y i = glue (x , y) i

open Homotopy.Pushout using (inl ; inr) public

We show that the join operation is associative by a direct cubical computation due to LoΓ―c Pujet. A more conceptual proof is given in (Univalent Foundations Program 2013, lemma 8.5.9).

join-associative : (X βˆ— Y) βˆ— Z ≃ X βˆ— (Y βˆ— Z)

join-associative .fst (inl (inl x)) = inl x
join-associative .fst (inl (inr y)) = inr (inl y)
join-associative .fst (inl (join x y i)) = join x (inl y) i
join-associative .fst (inr z) = inr (inr z)
join-associative .fst (join (inl x) z i) = join x (inr z) i
join-associative .fst (join (inr y) z i) = inr (join y z i)
join-associative .fst (join (join x y i) z j) =
  hcomp (βˆ‚ i ∨ βˆ‚ j) Ξ» where
    k (k = i0) β†’ join x (join y z j) i
    k (i = i0) β†’ join x (inr z) (j ∧ k)
    k (i = i1) β†’ inr (join y z j)
    k (j = i0) β†’ join x (inl y) i
    k (j = i1) β†’ join x (inr z) (i ∨ k)

join-associative {X = X} {Y = Y} {Z = Z} .snd = is-iso→is-equiv λ where
  .is-iso.from (inl x) β†’ inl (inl x)
  .is-iso.from (inr (inl y)) β†’ inl (inr y)
  .is-iso.from (inr (inr z)) β†’ inr z
  .is-iso.from (inr (join y z i)) β†’ join (inr y) z i
  .is-iso.from (join x (inl y) i) β†’ inl (join x y i)
  .is-iso.from (join x (inr z) i) β†’ join (inl x) z i
  .is-iso.from (join x (join y z j) i) β†’
    hcomp (βˆ‚ i ∨ βˆ‚ j) Ξ» where
      k (k = i0) β†’ join (join x y i) z j
      k (i = i0) β†’ join (inl x) z (j ∧ ~ k)
      k (i = i1) β†’ join (inr y) z j
      k (j = i0) β†’ inl (join x y i)
      k (j = i1) β†’ join (inl x) z (i ∨ ~ k)

  .is-iso.rinv (inl x) β†’ refl
  .is-iso.rinv (inr (inl y)) β†’ refl
  .is-iso.rinv (inr (inr z)) β†’ refl
  .is-iso.rinv (inr (join y z i)) β†’ refl
  .is-iso.rinv (join x (inl y) i) β†’ refl
  .is-iso.rinv (join x (inr z) i) β†’ refl
  .is-iso.rinv (join x (join y z j) i) l β†’
    comp (Ξ» _ β†’ X βˆ— (Y βˆ— Z)) (βˆ‚ i ∨ βˆ‚ j ∨ l) Ξ» where
      k (k = i0) β†’ hcomp (βˆ‚ i ∨ βˆ‚ j ∨ l) Ξ» where
        k (k = i0) β†’ join x (join y z j) i
        k (i = i0) β†’ join x (inr z) (j ∧ (k ∧ ~ l))
        k (i = i1) β†’ inr (join y z j)
        k (j = i0) β†’ join x (inl y) i
        k (j = i1) β†’ join x (inr z) (i ∨ (k ∧ ~ l))
        k (l = i1) β†’ join x (join y z j) i
      k (i = i0) β†’ join x (inr z) (j ∧ (~ k ∧ ~ l))
      k (i = i1) β†’ inr (join y z j)
      k (j = i0) β†’ join x (inl y) i
      k (j = i1) β†’ join x (inr z) (i ∨ (~ k ∧ ~ l))
      k (l = i1) β†’ join x (join y z j) i

  .is-iso.linv (inl (inl x)) β†’ refl
  .is-iso.linv (inl (inr y)) β†’ refl
  .is-iso.linv (inl (join x y i)) β†’ refl
  .is-iso.linv (inr z) β†’ refl
  .is-iso.linv (join (inl x) z i) β†’ refl
  .is-iso.linv (join (inr y) z i) β†’ refl
  .is-iso.linv (join (join x y i) z j) l β†’
    comp (Ξ» _ β†’ (X βˆ— Y) βˆ— Z) (βˆ‚ i ∨ βˆ‚ j ∨ l) Ξ» where
      k (k = i0) β†’ hcomp (βˆ‚ i ∨ βˆ‚ j ∨ l) Ξ» where
        k (k = i0) β†’ join (join x y i) z j
        k (i = i0) β†’ join (inl x) z (j ∧ (~ k ∨ l))
        k (i = i1) β†’ join (inr y) z j
        k (j = i0) β†’ inl (join x y i)
        k (j = i1) β†’ join (inl x) z (i ∨ (~ k ∨ l))
        k (l = i1) β†’ join (join x y i) z j
      k (i = i0) β†’ join (inl x) z (j ∧ (k ∨ l))
      k (i = i1) β†’ join (inr y) z j
      k (j = i0) β†’ inl (join x y i)
      k (j = i1) β†’ join (inl x) z (i ∨ (k ∨ l))
      k (l = i1) β†’ join (join x y i) z j

The join operation is also commutative; luckily, this is much more straightforward.

join-swap : X βˆ— Y β†’ Y βˆ— X
join-swap (inl x) = inr x
join-swap (inr x) = inl x
join-swap (join a b i) = join b a (~ i)

join-commutative : X βˆ— Y ≃ Y βˆ— X
join-commutative .fst = join-swap
join-commutative .snd = is-iso→is-equiv record where
  from = join-swap
  rinv = Pushout-elim (Ξ» _ β†’ refl) (Ξ» _ β†’ refl) Ξ» c i j β†’ glue c i
  linv = Pushout-elim (Ξ» _ β†’ refl) (Ξ» _ β†’ refl) Ξ» c i j β†’ glue c i

Finally, if either of the joined types is contractible, so is the join.

join-is-contr-l : is-contr X β†’ is-contr (X βˆ— Y)
join-is-contr-l h .centre = inl (centre h)
join-is-contr-l h .paths (inl x) = ap inl (paths h x)
join-is-contr-l h .paths (inr y) = join (centre h) y
join-is-contr-l h .paths (join x y i) j = hcomp (βˆ‚ i ∨ βˆ‚ j) Ξ» where
  k (k = i0) β†’ join x y (i ∧ j)
  k (i = i0) β†’ inl (paths h x (~ k ∨ j))
  k (i = i1) β†’ join (paths h x (~ k)) y j
  k (j = i0) β†’ inl (paths h x (~ k))
  k (j = i1) β†’ join x y i

join-is-contr-r : is-contr Y β†’ is-contr (X βˆ— Y)
join-is-contr-r h .centre = inr (centre h)
join-is-contr-r h .paths (inl x) = sym (join x (centre h))
join-is-contr-r h .paths (inr y) = ap inr (paths h y)
join-is-contr-r h .paths (join x y i) j = hcomp (βˆ‚ i ∨ βˆ‚ j) Ξ» where
  k (k = i0) β†’ join x y (i ∨ ~ j)
  k (i = i0) β†’ join x (paths h y (~ k)) (~ j)
  k (i = i1) β†’ inr (paths h y (~ k ∨ j))
  k (j = i0) β†’ inr (paths h y (~ k))
  k (j = i1) β†’ join x y i

join-map : (A β†’ B) β†’ (X β†’ Y) β†’ A βˆ— X β†’ B βˆ— Y
join-map f g (inl x) = inl (f x)
join-map f g (inr x) = inr (g x)
join-map f g (join a b i) = join (f a) (g b) i

join-ap : (A ≃ B) β†’ (X ≃ Y) β†’ A βˆ— X ≃ B βˆ— Y
join-ap f g .fst = join-map (f .fst) (g .fst)
join-ap f g .snd = is-iso→is-equiv record where
  from = join-map (Equiv.from f) (Equiv.from g)
  rinv = Pushout-elim (Ξ» b β†’ ap inl (Equiv.Ξ΅ f b)) (Ξ» y β†’ ap inr (Equiv.Ξ΅ g y))
      Ξ» (b , y) i j β†’ join (Equiv.Ξ΅ f b j) (Equiv.Ξ΅ g y j) i
  linv = Pushout-elim (Ξ» a β†’ ap inl (Equiv.Ξ· f a)) (Ξ» x β†’ ap inr (Equiv.Ξ· g x))
      Ξ» (a , x) i j β†’ join (Equiv.Ξ· f a j) (Equiv.Ξ· g x j) i

Suspensions as joinsπŸ”—

The suspension of is equivalently the join of with the booleans: the two booleans correspond to the poles, and the meridian passing through corresponds to the composite path Notice that the map sends every to the south pole. This is arbitrary, and we could just as well have chosen the north pole; all the information lives in the meridians.

2βˆ—β‰‘Susp : Bool βˆ— A ≃ Susp A
2βˆ—β‰‘Susp .fst (inl true)  = north
2βˆ—β‰‘Susp .fst (inl false) = south
2βˆ—β‰‘Susp .fst (inr x) = south
2βˆ—β‰‘Susp .fst (join true  a i) = merid a i
2βˆ—β‰‘Susp .fst (join false _ i) = south

2βˆ—β‰‘Susp .snd = is-isoβ†’is-equiv record where
  from = Susp-elim _ (inl true) (inl false) Ξ» a β†’ join true a βˆ™ sym (join false a)
  rinv = Susp-elim _ refl refl Ξ» a β†’
    transpose (ap-βˆ™ (2βˆ—β‰‘Susp .fst) (join true a) (sym (join false a)) βˆ™ βˆ™-idr _)
  linv = Pushout-elim
    (Ξ» { true β†’ refl
        ; false β†’ refl })
    (Ξ» a β†’ join false a)
    Ξ» { (true , a) β†’ transpose (flip₁ (βˆ™-filler _ _))
      ; (false , a) i j β†’ join false a (i ∧ j) }

Joins of propositionsπŸ”—

When applied to propositions, the join construction acts as logical disjunction. If X and Y are propositions, then X βˆ— Y is also a proposition, which holds iff either X or Y does.

join-elim-prop : {P : X βˆ— Y β†’ Type β„“} (pprop : βˆ€ x β†’ is-prop (P x))
  β†’ (f : βˆ€ x β†’ P (inl x)) (g : βˆ€ y β†’ P (inr y))
  β†’ βˆ€ x β†’ P x
join-elim-prop h f g =
  Pushout-elim f g λ c → is-prop→pathp (λ i → h (glue c i)) _ _

join-is-prop : is-prop X β†’ is-prop Y β†’ is-prop (X βˆ— Y)
join-is-prop {X = X} {Y = Y} hx hy = Ξ» x y β†’ go x x y where
  go : X βˆ— Y β†’ is-prop (X βˆ— Y)
  go = join-elim-prop
    (Ξ» _ β†’ is-prop-is-prop)
    (Ξ» x β†’ is-contrβ†’is-prop (join-is-contr-l (is-propβˆ™β†’is-contr hx x)))
    (Ξ» y β†’ is-contrβ†’is-prop (join-is-contr-r (is-propβˆ™β†’is-contr hy y)))

References