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


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