Homotopy Type Theory
wedge sum (Rev #5, changes)

Showing changes from revision #4 to #5: Added | Removed | Changed


We can stick to 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+BA veeBB in : A + B \to A \veeB \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.