Homotopy Type Theory join > history (Rev #2, changes)

In classical algebraic topology the 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

References

• The join construction, Egbert Rijke
• HoTT book