Homotopy Type Theory
pushout (Rev #3, changes)

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


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.


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

  • a function inl:AA C CB inl : A \to A \sqcup_{C} \sqcup^{C} B
  • a function inr:BA C CB inr : B \to A \sqcup_{C} \sqcup^{C} B
  • for each c:Cc:C a path glue(c):inl(f(c))=inr(g(c))glue(c) : inl (f (c)) = inr (g( c))


See also

Synthetic homotopy theory


HoTT Book

category: homotopy theory

Revision on September 5, 2018 at 08:11:31 by Ali Caglayan. See the history of this page for a list of all contributions to it.