Homotopy Type Theory
smash product (Rev #5, changes)

Showing changes from revision #4 to #5: Added | Removed | Changed


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

1ABA×B\mathbf 1 \leftarrow A \wedge B \rightarrow A \times B

where ABA×BA \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 ABA \wedge B and is pointed by ABinl( 1)\star_{A \wedge B}\equiv\mathrm{inl}(\star_{\mathbf 1})

It can also be defined as the pushout of the span

2A+BA×B\mathbf{2} \leftarrow A + B \rightarrow A \times B



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.