wedge sum (Rev #4, changes)

Showing changes from revision #3 to #4:
Added | ~~Removed~~ | ~~Chan~~ged

~~ The~~ We~~ wedge~~ can~~ sum~~ stick~~ of~~ to~~ two~~ spaces~~ types~~ together by their points.~~$A$~~~~ and ~~~~$B$~~~~, can 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)$

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 \veeB$
- 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)$

category: homotopy theory

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