Homotopy Type Theory
wedge sum


We can stick two spaces together by their points.


The wedge sum of two pointed types (A,a)(A,a) and (B,b)(B,b) can be defined as the higher inductive type with the following constructors:

The wedge sum of two types AA and BB, can also 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)


HoTT book

category: homotopy theory