Homotopy Type Theory pushout > history (Rev #2, changes)

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

Idea

~~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))$

Definition

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

Examples

References

HoTT Book

category: homotopy theory

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