Homotopy Type Theory
pushout

Idea

Many constructions in homotopy theory are special cases of pushouts. Although when being defined sometimes it may be clearer to define the construction as a seperate higher inductive type and then later on prove it is equivalent? to the pushout definition.

Definition

The (homotopy) pushout of a span AfCgBA \xleftarrow{f} C \xrightarrow{g} B is the higher inductive type A f;g CBA \sqcup^{C}_{f ; g} B (or A CBA \sqcup^C B) generated by:

Examples

See also

Synthetic homotopy theory

References

HoTT Book

category: homotopy theory