Wedge Sum of Pointed Types

The wedge sum of a family $X_{i}:I\to\mathsf{U}{}_{\bullet}$ of Pointed Types is given by the Wide Pushout along the maps $\mathrm{pt}_{i}:\top\to X_{i}$ that selects out all the base points. When Set Truncated, this gives the wedge sum of pointed sets, denoted $\bigvee_{i:I}X_{i}$.

Properties

• The wedge sum of pointed sets is the Indexed Coproduct of a family of pointed sets $(X_{i},\mathrm{pt}_{i})$. The universal properties all come directly from the construction via wide pushouts.

  An alternative way to see this is that the aforementioned pushout is precisely how we compute Indexed Coproducts in Coslice Categories.