[[!redirects pushout]] ## 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](https://homotopytypetheory.org/book/) [[!redirects Homotopy pushout]]