# Kerodon

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

Proposition 3.4.1.2. Suppose we are given a commutative diagram of simplicial sets

3.38
$$\label{diagram:homotopy-pullback-square1} \begin{gathered} \xymatrix@R =50pt@C=50pt{ X_{01} \ar [r] \ar [d] & X_0 \ar [d]^{q} \\ X_1 \ar [r] & X. } \end{gathered}$$

Suppose that $q$ factors as a composition $X_0 \xrightarrow {w'} X'_0 \xrightarrow {q'} X$, where $w'$ is a weak homotopy equivalence and $q'$ is a Kan fibration. Then (3.38) is a homotopy pullback square if and only if the induced map $\rho ': X_{01} \rightarrow X'_{0} \times _{X} X_1$ is a weak homotopy equivalence.

Proof. Suppose that $q$ admits another factorization $X_0 \xrightarrow {w''} X''_0 \xrightarrow { q''} X$, where $w''$ is a weak homotopy equivalence and $q''$ is a Kan fibration. We wish to show that $\rho '$ is a weak homotopy equivalence if and only if the induced map $\rho '': X_{01} \rightarrow X'_{0} \times _{X} X_1$ is a weak homotopy equivalence. To prove this equivalence, we may assume without loss of generality that $w'$ is anodyne (since this can always be arranged using Proposition 3.1.7.1). In this case, the lifting problem

$\xymatrix@R =50pt@C=50pt{ X_0 \ar [d]^{ w' } \ar [r]^-{w''} & X''_0 \ar [d]^{q''} \\ X'_0 \ar@ {-->}[ur]^{u} \ar [r]^-{q'} & X }$

admits a solution $u: X'_0 \rightarrow X''_0$ (Remark 3.1.2.7). Since $w'$ and $w''$ are weak homotopy equivalences, the equality $w'' = u \circ w'$ guarantees that $u$ is also a weak homotopy equivalence (Remark 3.1.6.16), so that the map $X'_0 \times _{X} X_1 \rightarrow X''_0 \times _{X} X_1$ is a weak homotopy equivalence by virtue of Proposition 3.4.0.2. $\square$