[[!redirects Smash product]] ## Idea ## The smash product of two [[pointed type]]s A,B can be defined as the [[pushout]] of the span $$\mathbf 1 \leftarrow A \wedge B \rightarrow A \times B$$ 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})$ ## Definition ## ## References ## * [[HoTT book]] * [On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory](http://florisvandoorn.com/papers/dissertation.pdf) * [Higher-Dimensional Types in the Mechanization of Homotopy Theory](https://favonia.org/files/thesis.pdf) category: homotopy theory