Homotopy Type Theory


In classical algebraic topology the join of topological spaces of two spaces XX and YY can be thought as a cone over XX with tip the shape of YY.

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?.


The join of a type AA and BB is the pushout of the following span

AfstA×BsndBA \xleftarrow{\text{fst}} A \times B \xrightarrow{\text{snd}} B