# Kerodon

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

Proposition 3.4.3.2. Suppose we are given a homotopy coCartesian diagram of simplicial sets

3.50
\begin{equation} \label{equation:mather-second-cube} \begin{gathered} \xymatrix { A \ar [r]^{f} \ar [d] & B \ar [d] \\ C \ar [r] & D, } \end{gathered} \end{equation}

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

$\xymatrix { 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 homotopy coCartesian.

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.6.11). Set $D' = B' \coprod _{A} C$. Our assumption that (3.50) is a homotopy pushout square guarantees that the induced map $D' \rightarrow D$ is a weak homotopy equivalence (Remark 3.4.2.8). We have a commutative diagram of simplicial sets

$\xymatrix { 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 homotopy coCartesian (Example 3.4.2.7). 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 homotopy coCartesian (Proposition 3.4.2.5). Applying Proposition 3.4.2.3, we deduce that the outer rectangle is also homotopy coCartesian, as desired. $\square$