# Kerodon

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

Corollary 4.5.7.4. A commutative diagram of $\infty$-categories

4.42
$$\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}$$

is a categorical pullback square if and only if the induced diagram of Kan complexes

4.43
$$\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}$$

is a homotopy pullback square.

Proof. We proceed as in the proof of Proposition 4.5.2.12. By definition, the diagram (4.42) 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.5 and 4.5.2.5, 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.43). The desired result now follows from the criterion of Corollary 3.4.1.6. $\square$