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

Showing changes from revision #1 to #2: Added | Removed | Changed

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

## References

HoTT Book

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.