Homotopy Type Theory smash product > history (Rev #8, changes)

Idea

The smash product of two pointed types $A,B$ can be defined as the pushout of the span

where $A \wedge B \rightarrow A \times B$ is the inclusion of the wedge sum in the product type? both of which are pointed. The resulting pushout is denoted the smash product $A \wedge B$ and is pointed by $\star_{A \wedge B}\equiv\mathrm{inl}(\star_{\mathbf 1})$

It can also be defined as the pushout of the span

Definition

References

• HoTT book
• On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory
• Higher-Dimensional Types in the Mechanization of Homotopy Theory