## Idea ## The wedge sum of two types $A$ and $B$, can be defined as the [[pushout]] of the span $$A \leftarrow \mathbf{1} \rightarrow B$$ where the maps pick the base points of $A$ and $B$. This pushout is denoted $A \vee B$ and has basepoint $\star_{A \vee B} \equiv \mathrm{inl}(\star_A)$ ## Definition ## ## References ##