# Kerodon

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

Proposition 5.2.6.24. Suppose we are given a pullback diagram of simplicial sets

$\xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}' \ar [d] \ar [r]^-{F} & \operatorname{\mathcal{C}}\ar [d]^-{q} \\ \operatorname{\mathcal{D}}' \ar [r]^-{\overline{F}} & \operatorname{\mathcal{D}}, }$

where $\operatorname{\mathcal{D}}$ is an $\infty$-category and $\overline{F}$ is a categorical equivalence of simplicial sets. If $q$ is either a cartesian fibration or a cocartesian fibration, then $F$ is also a categorical equivalence of simplicial sets.

Proof of Proposition 5.2.6.24. Suppose we are given a pullback square

$\xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}' \ar [d] \ar [r]^-{F} & \operatorname{\mathcal{C}}\ar [d]^-{q} \\ \operatorname{\mathcal{D}}' \ar [r]^-{\overline{F}} & \operatorname{\mathcal{D}}, }$

where $q$ is a cocartesian fibration of $\infty$-categories and $\overline{F}$ is a categorical equivalence; we wish to show that $F$ is also a categorical equivalence (the analogous assertion for cartesian fibrations follows by a similar argument). By virtue of Proposition 4.1.3.2, the morphism $\overline{F}$ factors as a composition

$\operatorname{\mathcal{D}}' \xrightarrow { \overline{F}' } \operatorname{\mathcal{D}}'' \xrightarrow { \overline{F}'' } \operatorname{\mathcal{D}},$

where $\overline{F}'$ is inner anodyne and $\overline{F}''$ is an inner fibration. Since $\operatorname{\mathcal{D}}$ is an $\infty$-category, it follows that $\operatorname{\mathcal{D}}''$ is also an $\infty$-category (Remark 4.1.1.9). Because $\overline{F}'$ is a categorical equivalence (Corollary 4.5.2.13), our assumption that $\overline{F}$ is a categorical equivalence guarantees that $\overline{F}''$ is an equivalence of $\infty$-categories (Remark 4.5.2.5). Proposition 5.1.4.8 guarantees that $q$ is an isofibration of $\infty$-categories, so that the projection map $\operatorname{\mathcal{D}}'' \times _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}$ is also an equivalence of $\infty$-categories (Corollary 4.5.4.6). It will therefore suffice to show that $\overline{F}'$ induces a categorical equivalence $\operatorname{\mathcal{C}}' \simeq \operatorname{\mathcal{D}}' \times _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{C}}\hookrightarrow \operatorname{\mathcal{D}}'' \times _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{C}}$, which is a special case of Lemma 5.2.6.26. $\square$