Homotopy Type Theory
wedge sum (Rev #5)


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:

  • Points come from the sum type? in:A+BABin : A + B \to A \vee B
  • And their base point is glued path:inl(a)=inr(b)path : inl(a) = inr(b) Clearly this is pointed.

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

Revision on January 19, 2019 at 10:54:32 by Ali Caglayan. See the history of this page for a list of all contributions to it.