## Idea In classical algebraic topology the [[nlab:join of topological spaces]] of two spaces $X$ and $Y$ can be thought as a cone over $X$ with tip the shape of $Y$. Joins come up in many constructions in homotopy type theory especially in [[synthetic homotopy theory]]. The join of two types is the pushout of the projection maps from their product. There is also a related notion of the [[join of maps]]. ## Definition The join of a [[type]] $A$ and $B$ is the pushout of the following span $$A \xleftarrow{\text{fst}} A \times B \xrightarrow{\text{snd}} B$$ ## References * [[The join construction]], [[Egbert Rijke]] * [[HoTT book]]