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 seperateAfCgBA \xleftarrow{f} C \xrightarrow{g} B is the higher inductive type and then later on prove it isA CBA \sqcup_{C} Bequivalent? generated to by: the pushout definition.

  • a function inl:AA CBinl : A \to A \sqcup_{C} B
  • a function inr:BA CBinr : B \to A \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))

Definition

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

  • a function inl:AA CBinl : A \to A \sqcup_{C} B
  • a function inr:BA CBinr : B \to A \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))

Examples

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.