Contents

# Contents

## 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$