# Homotopy Type Theory join

## Idea

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

$A \xleftarrow{\text{fst}} A \times B \xrightarrow{\text{snd}} B$

## References

Created on February 14, 2019 at 11:59:41. See the history of this page for a list of all contributions to it.