$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Corollary 4.5.7.4. A commutative diagram of $\infty $-categories
4.43
\begin{equation} \begin{gathered}\label{equation:categorical-pullback-square29} \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}_{01} \ar [r] \ar [d] & \operatorname{\mathcal{C}}_0 \ar [d]^{U} \\ \operatorname{\mathcal{C}}_1 \ar [r] & \operatorname{\mathcal{C}}. } \end{gathered} \end{equation}
is a categorical pullback square if and only if the induced diagram of Kan complexes
4.44
\begin{equation} \begin{gathered}\label{equation:bellie} \xymatrix@R =50pt@C=50pt{ \operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{C}}_{01} )^{\simeq } \ar [r] \ar [d] & \operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{C}}_{0} )^{\simeq } \ar [d] \\ \operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{C}}_{1} )^{\simeq } \ar [r] & \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}})^{\simeq } } \end{gathered} \end{equation}
is a homotopy pullback square.
Proof.
We proceed as in the proof of Proposition 4.5.2.14. By definition, the diagram (4.43) is a categorical pullback square if and only if the induced map $\theta : \operatorname{\mathcal{C}}_{01} \rightarrow \operatorname{\mathcal{C}}_{0} \times ^{\mathrm{h}}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_1$ is an equivalence of $\infty $-categories. Using the criterion of Theorem 4.5.7.1, we see that this is equivalent to the requirement that $\theta $ induces a homotopy equivalence of Kan complexes $\rho : \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}}_{01} )^{\simeq } \rightarrow \operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{C}}_{0} \times ^{\mathrm{h}}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_1)^{\simeq }$. Using Remarks 4.5.2.6 and 4.5.2.7, we can identify $\rho $ with the map
\[ \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}}_{01} )^{\simeq } \rightarrow \operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{C}}_0)^{\simeq } \times ^{\mathrm{h}}_{\operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{C}})^{\simeq } } \operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{C}}_1)^{\simeq } \]
determined by the commutative diagram (4.44). The desired result now follows from the criterion of Corollary 3.4.1.6.
$\square$