# Kerodon

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

Corollary 3.4.1.5. Suppose we are given a commutative diagram of simplicial sets

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

where $q$ is a weak homotopy equivalence. Then (3.42) is a homotopy pullback square if and only if $q'$ is a weak homotopy equivalence.

Proof. Apply Proposition 3.4.1.2 to the factorization $q = \operatorname{id}_{X} \circ q$. $\square$