pushout (Rev #2, changes)

Showing changes from revision #1 to #2:
Added | ~~Removed~~ | ~~Chan~~ged

~~ The~~ Many~~ (homotopy)~~ constructions~~ pushout~~ in homotopy theory are special cases of pushouts. Although when being defined sometimes it may be clearer to define the construction as a~~ span~~ seperate~~$A \xleftarrow{f} C \xrightarrow{g} B$~~~~ is the ~~higher inductive type and then later on prove it is~~$A \sqcup_{C} B$~~equivalent? ~~ generated~~ to~~ by:~~ the pushout definition.

- a function $inl : A \to A \sqcup_{C} B$
- a function $inr : B \to A \sqcup_{C} B$
- for each $c:C$ a path $glue(c) : inl (f (c)) = inr (g( c))$

The (homotopy) pushout of a span $A \xleftarrow{f} C \xrightarrow{g} B$ is the higher inductive type $A \sqcup_{C} B$ generated by:

- a function $inl : A \to A \sqcup_{C} B$
- a function $inr : B \to A \sqcup_{C} B$
- for each $c:C$ a path $glue(c) : inl (f (c)) = inr (g( c))$

category: homotopy theory

Revision on September 4, 2018 at 05:34:19 by Ali Caglayan. See the history of this page for a list of all contributions to it.