$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Proposition 7.5.4.13. Suppose we are given a commutative diagram of simplicial sets
7.56
\begin{equation} \begin{gathered}\label{equation:homotopy-pullback-as-homotopy-limit} \xymatrix@R =50pt@C=50pt{ X_{01} \ar [r] \ar [d] & X_{0} \ar [d] \\ X_{1} \ar [r] & X, } \end{gathered} \end{equation}
which we identify with a functor $\mathscr {F}: [1] \times [1] \rightarrow \operatorname{Set_{\Delta }}$. Then (7.56) is a homotopy pullback square (in the sense of Definition 3.4.1.1) if and only if $\mathscr {F}$ is a homotopy limit diagram (in the sense of Definition 7.5.4.8).
Proof.
Using Proposition 3.1.7.1, we can choose a levelwise weak homotopy equivalence $\alpha : \mathscr {F} \rightarrow \mathscr {F}'$, where $\mathscr {F}'$ is a diagram of Kan complexes. Using Corollaries 3.4.1.12 and 7.5.4.11, we can replace $\mathscr {F}$ by $\mathscr {F}'$ and thereby reduce to the case where (7.56) is a diagram of Kan complexes. By virtue of Corollary 3.4.1.6, the diagram (7.56) is a homotopy pullback square if and only if it induces a homotopy equivalence $f: X_{01} \rightarrow X_{0} \times _{X}^{\mathrm{h}} X_1$, where $X_0 \times _{X}^{\mathrm{h}} X_{1}$ is the homotopy fiber product of Construction 3.4.0.3. On the other hand, $\mathscr {F}$ is a homotopy limit diagram if and only if the composition $\iota \circ f$ is a homotopy equivalence, where
\[ \iota : X_{0} \times _{X}^{\mathrm{h}} X_{1} \hookrightarrow X_0 \times ^{\mathrm{h}}_{X} ( X_{1} \times ^{\mathrm{h}}_{X} X) \simeq \underset {\longleftarrow }{\mathrm{holim}}(F) \]
is the comparison map described in Example 7.5.2.17. The desired result now follows from the observation that $\iota $ is a homotopy equivalence (see Example 7.5.2.17).
$\square$