smash product (Rev #5, changes)

Showing changes from revision #4 to #5:
Added | ~~Removed~~ | ~~Chan~~ged

The smash product of two pointed~~ type~~ types~~ s~~~~ A,B~~~~ can~~~~ be~~~~ defined~~~~ as~~~~ the~~$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})$

It can also be defined as the pushout of the span

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

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

category: homotopy theory

Revision on October 14, 2018 at 09:27:02 by Ali Caglayan. See the history of this page for a list of all contributions to it.