[[!redirects Pushout]] [[!redirects pushout]] ## 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 \sqcup^{C}_{f ; g} B$ (or $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))$ ## Examples ## * [[suspension]] * [[wedge sum]] * [[smash product]] ## See also ## [[Synthetic homotopy theory]] ## References ## [HoTT Book](https://homotopytypetheory.org/book/) [[!redirects Homotopy pushout]] category: homotopy theory