open import 1Lab.Prelude

open import Homotopy.Pushout

module Homotopy.Join where

The join of types🔗

private variable
  ℓ ℓ' : Level
  X Y Z : Type ℓ

The join of two types $A$ and $B$ is the pushout under the diagram $$A\leftarrow (A\times B)\to B\text{.}$$

_∗_ : Type ℓ → Type ℓ' → Type (ℓ ⊔ ℓ')
A ∗ B = Pushout (A × B) fst snd

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

open Homotopy.Pushout using (inl ; inr) public