Homotopy Type Theory
wedge sum

Idea

We can stick two spaces together by their points.

Definition

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)

References

HoTT book

category: homotopy theory