# Kerodon

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

Corollary 5.6.4.6. Suppose we are given a pullback diagram of simplicial sets

5.53
$$\begin{gathered}\label{equation:pullback-cocartesian-fibration} \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}\ar [r]^-{ \widetilde{F} } \ar [d]^{U} & \operatorname{\mathcal{E}}' \ar [d]^{U'} \\ \operatorname{\mathcal{C}}\ar [r]^-{F} & \operatorname{\mathcal{C}}', } \end{gathered}$$

where $U'$ is a cocartesian fibration. If $F$ is a categorical equivalence of simplicial sets, then $\widetilde{F}$ is also a categorical equivalence of simplicial sets.

Proof. Using Corollary 5.6.4.3, we can extend (5.53) to a diagram of pullback squares

$\xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}\ar [r]^-{ \widetilde{F} } \ar [d]^{U} & \operatorname{\mathcal{E}}' \ar [d]^{U'} \ar [r] & \operatorname{\mathcal{E}}'' \ar [d]^{U''} \\ \operatorname{\mathcal{C}}\ar [r]^-{F} & \operatorname{\mathcal{C}}' \ar [r]^-{G} & \operatorname{\mathcal{C}}'' }$

where $U''$ is a cocartesian fibration, $G$ is inner anodyne, and $\operatorname{\mathcal{C}}''$ is an $\infty$-category. Since $G$ and $G \circ F$ are categorical equivalences, it follows from Proposition 5.2.6.24 that $\widetilde{G}$ and $\widetilde{G} \circ \widetilde{F}$ are categorical equivalences. Applying the two-out-of-three property (Remark 4.5.2.5), we conclude that $\widetilde{F}$ is also a categorical equivalence. $\square$