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

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

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 $A \xleftarrow{f} C \xrightarrow{g} B$ is the higher inductive type $A{\bigsqcup }_C{\bigsqcup }_{f;g}^{C}B$ A \sqcup_{C} \sqcup^{C}_{f ; g} B generated (or by:$A \sqcup^C B$) generated by:

• a function $\mathrm{inl}:A\to A{\bigsqcup }_C{\bigsqcup }^{C}B$ inl : A \to A \sqcup_{C} \sqcup^{C} B
• a function $\mathrm{inr}:B\to A{\bigsqcup }_C{\bigsqcup }^{C}B$ inr : B \to A \sqcup_{C} \sqcup^{C} B
• for each $c:C$ a path $glue(c) : inl (f (c)) = inr (g( c))$

Examples

• suspension
• wedge sum
• smash product

References

HoTT Book