Homotopy Type Theory
wedge sum (Rev #3)


The wedge sum of two types AA and BB, can be defined as the pushout of the span

A1BA \leftarrow \mathbf{1} \rightarrow B

where the maps pick the base points of AA and BB. This pushout is denoted ABA \vee B and has basepoint ABinl( A)\star_{A \vee B} \equiv \mathrm{inl}(\star_A)



category: homotopy theory

Revision on September 4, 2018 at 09:35:24 by Ali Caglayan. See the history of this page for a list of all contributions to it.