# Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$ $\newcommand\empty{}$

Proposition 3.4.3.2. Suppose we are given a homotopy pushout square of simplicial sets

3.52
$$\label{equation:mather-second-cube} \begin{gathered} \xymatrix@R =50pt@C=50pt{ A \ar [r]^-{f} \ar [d] & B \ar [d] \\ C \ar [r] & D, } \end{gathered}$$

and let $q: \overline{D} \rightarrow D$ be a Kan fibration of simplicial sets. Then the induced diagram

$\xymatrix@R =50pt@C=50pt{ A \times _{D} \overline{D} \ar [r] \ar [d] & B \times _{D} \overline{D} \ar [d] \\ C \times _{D} \overline{D} \ar [r] & \overline{D} }$

is also a homotopy pushout square.

Proof. Choose a factorization of $f$ as a composition $A \xrightarrow {f'} B' \xrightarrow {w} B$, where $f'$ is a monomorphism and $w$ is a weak homotopy equivalence (Exercise 3.1.7.10). Set $D' = B' \coprod _{A} C$. Our assumption that (3.52) is a homotopy pushout square guarantees that the induced map $D' \rightarrow D$ is a weak homotopy equivalence (Proposition 3.4.2.11). We have a commutative diagram of simplicial sets

$\xymatrix@R =50pt@C=50pt{ A \times _{D} \overline{D} \ar [r] \ar [d] & B' \times _{D} \overline{D} \ar [r] \ar [d] & B \times _{D} \overline{D} \ar [d] \\ C \times _{D} \overline{D} \ar [r] & D' \times _{D} \overline{D} \ar [r] & \overline{D}. }$

The left square in this diagram is a pushout square (by virtue of Exercise 3.4.3.1) and the map $A \times _{D} \overline{D} \rightarrow B' \times _{D} \overline{D}$ is a monomorphism, so it is a homotopy pushout square (Example 3.4.2.12). It follows from Corollary 3.3.7.2 that the horizontal maps on the right side of the diagram are weak homotopy equivalences, so the right square is also a homotopy pushout (Proposition 3.4.2.10). Applying Proposition 3.4.2.8, we deduce that the outer rectangle is also a homotopy pushout square, as desired. $\square$