Homotopy pushout (source code)

= Homotopy pushout

For maps $A\to X$ and $A\to Y$, the double <mapping cylinder> $X\sqcup(A\times I)\sqcup Y$, with each endpoint attached by its given map, models the homotopy pushout. A map out of this model is a pair of maps on $X$ and $Y$ together with a <homotopy> between their restrictions to $A$. This is why compatible <homotopy classes> extend over a homotopy pushout. For a <CW pair>, the inclusion is a <cofibration> and the ordinary pushout gives the same homotopy type.