[[!redirects Wedge sum]] ## Idea ## We can stick two spaces together by their points. ## Definition ## The wedge sum of two pointed types $(A,a)$ and $(B,b)$ can be defined as the [[higher inductive type]] with the following constructors: * Points come from the [[sum type]] $in : A + B \to A \vee B$ * And their base point is glued $path : inl(a) = inr(b)$ Clearly this is pointed. The wedge sum of two types $A$ and $B$, can also 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)$ ## References ## [[HoTT book]] category: homotopy theory