nLab smash product type

Idea

The smash product type is an axiomatization of the smash product in the context of homotopy type theory.

Definition

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

$$\mathbf 1 \leftarrow A \vee B \rightarrow A \times B$$

where $A \vee B \rightarrow A \times B$ is the inclusion of the wedge sum type 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 type of the span

$$\mathbf{2} \leftarrow A + B \rightarrow A \times B$$

See also

• higher inductive type

• smash product

References

• Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)

• Floris van Doorn (2018), On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory, (arXiv:1808.10690, web)

• Kuen-Bang Hou, Higher-Dimensional Types in the Mechanization of Homotopy Theory, Ph. D. Thesis 2017 (web)