Homotopy Type Theory
wedge sum (Rev #5)

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:

  • 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)

References

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.