Homotopy Type Theory pushout > history (Rev #1)

Idea

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

Definition

References

HoTT Book