module Homotopy.Join where
The join of typesπ
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
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
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) }
References
- Univalent Foundations Program, The. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study: https://homotopytypetheory.org/book.