# Kerodon

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

Proposition 5.3.6.1. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a functor of $\infty$-categories which is either a cartesian fibration or a cocartesian fibration. Then $U$ is exponentiable (in the sense of Definition 4.5.9.10). That is, if we are given any diagram of simplicial sets

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

where both squares are pullbacks and $\overline{F}$ is a categorical equivalence, then $F$ is also a categorical equivalence.

Proof of Proposition 5.3.6.1. Without loss of generality we may assume that $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ is a cocartesian fibration of $\infty$-categories. Suppose we are given a commutative diagram of simplicial sets

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

where both squares are pullbacks and $\overline{F}$ is a categorical equivalence. We wish to show that $F$ is also a categorical equivalence. By virtue of Proposition 4.1.3.2, the morphism $\overline{G}$ factors as a composition $\operatorname{\mathcal{C}}' \xrightarrow {\overline{G}'} \operatorname{\mathcal{B}}\xrightarrow { \overline{G}'' } \operatorname{\mathcal{C}}$, where $\overline{G}'$ is inner anodyne and $\overline{G}''$ is an inner fibration. Note that the projection map $V: \operatorname{\mathcal{B}}\times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{B}}$ is a cocartesian fibration of $\infty$-categories. We may therefore replace $\operatorname{\mathcal{C}}$ by $\operatorname{\mathcal{B}}$ and thereby reduce to the special case where $\overline{G}$ is inner anodyne. In this case, the morphism $G: \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{E}}$ is a categorical equivalence of simplicial sets (Lemma 5.3.6.5). Consequently, to show that $F$ is a categorical equivalence of simplicial sets, it will suffice to show that the composite map $(G \circ F): \operatorname{\mathcal{E}}'' \rightarrow \operatorname{\mathcal{E}}$ is a categorical equivalence of simplicial sets (Remark 4.5.3.5).

Since $\overline{F}$ is a categorical equivalence and $\overline{G}$ is inner anodyne, it follows that the composite map $\overline{G} \circ \overline{F}: \operatorname{\mathcal{C}}'' \rightarrow \operatorname{\mathcal{C}}$ is also a categorical equivalence. Applying Proposition 4.1.3.2, we can factor $\overline{G} \circ \overline{F}$ as a composition $\operatorname{\mathcal{C}}'' \xrightarrow {\overline{F}_0} \operatorname{\mathcal{C}}'_0 \xrightarrow {\overline{G}_0} \operatorname{\mathcal{C}}$, where $\overline{F}_0$ is inner anodyne and $\overline{G}_0$ is an inner fibration. Since $\operatorname{\mathcal{C}}$ is an $\infty$-category, it follows that $\operatorname{\mathcal{C}}'_0$ is also an $\infty$-category (Remark 4.1.1.9). Set $\overline{\operatorname{\mathcal{E}}}'_0 = \operatorname{\mathcal{C}}'_{0} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$, so that we have a commutative diagram

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

satisfying $G \circ F = G_0 \circ F_0$. Since $U$ is an isofibration (Proposition 5.1.4.8) and $\overline{G}_0$ is an equivalence of $\infty$-categories, it follows that $G_0$ is an equivalence $\infty$-categories (Corollary 4.5.2.23). Applying Lemma 5.3.6.5 to the square on the left, we see that $F_0$ is a categorical equivalence of simplicial sets. Invoking Remark 4.5.3.5, we deduce that $G \circ F = G_0 \circ F_0$ is also a categorical equivalence, as desired. $\square$