Kerodon

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

Corollary 7.6.4.10. Suppose we are given a commutative diagram

7.65
\begin{equation} \begin{gathered}\label{equation:all-squares-in-SSet} \xymatrix@R =50pt@C=50pt{ X_{01} \ar [r] \ar [d] & X_{0} \ar [d] \\ X_1 \ar [r] & X } \end{gathered} \end{equation}

in the $\infty $-category $\operatorname{\mathcal{S}}$, classified by a map of Kan complexes

\[ g: X_{01} \rightarrow X_{0} \times ^{\mathrm{h}}_{ X} ( X_1 \times ^{\mathrm{h}}_{X} X ). \]

Then (7.65) is a pullback square in $\operatorname{\mathcal{S}}$ if and only if $g$ is a homotopy equivalence.