Kerodon

Proof. Using Theorem 9.4.4.1, we can choose a diagram

which exhibits $\widehat{\operatorname{\mathcal{E}}}^{\operatorname{op}}$ as a fiberwise $\kappa $-cocompletion of $\operatorname{\mathcal{E}}^{\operatorname{op}}$. Since $U$ is flat, the inner fibration $U^{\operatorname{op}}$ is also flat (Remark 9.4.6.5). Applying the criterion of Proposition 9.4.6.9, we see that $\widehat{U}^{\operatorname{op}}$ is a cartesian fibration. Let $\lambda $ be a regular cardinal of exponential cofinality $\geq \kappa $ such that $\widehat{U}$ is essentially $\lambda $-small. Let $h^{+}$ denote the composition of $h$ with the inclusion functor

We will complete the proof by showing that $h^{+}$ is fully faithful.

Since $\lambda $ has exponential cofinality $\geq \kappa $, the $\infty $-category $\operatorname{\mathcal{S}}^{< \lambda }$ admits $\kappa $-small limits (Example 7.6.6.4). Let $\operatorname{Fun}( \widehat{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \lambda } )$ denote the relative exponential of Construction 4.5.9.1. By definition, objects of $\operatorname{Fun}( \widehat{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \lambda } )$ can be identified with pairs $(C, \mathscr {G} )$, where $C$ is an object of $\operatorname{\mathcal{C}}$ and $\mathscr {G}: \widehat{\operatorname{\mathcal{E}}}_{C} \rightarrow \operatorname{\mathcal{S}}^{< \lambda }$ is a functor. Let $\operatorname{Fun}'( \widehat{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \lambda } )$ be the full subcategory spanned by those pairs $(C, \mathscr {F} )$, where the functor $\mathscr {G}$ preserves $\kappa $-small limits. Let $\widehat{H}: \widehat{\operatorname{\mathcal{E}}}^{\operatorname{op}} \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \times _{\operatorname{\mathcal{C}}} \widehat{\operatorname{\mathcal{E}}} \rightarrow \operatorname{\mathcal{S}}^{< \lambda }$ be a relative $\operatorname{Hom}$-functor for $\widehat{U}$, which we identify with a map

Since corepresentable functors preserve limits (Corollary 7.4.1.19), the functor $\widehat{h}$ factors through the full subcategory $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{Tw}(\operatorname{\mathcal{C}}) / \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{Fun}'( \widehat{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \lambda } ))$. Since $F$ is fully faithful (Remark 9.4.1.14), the functor $h^{+}$ is isomorphic to the composition

where $T$ is given by precomposition with $F$. It follows from the universal property of Theorem 9.4.1.20 that precomposition with $F$ induces an equivalence $\operatorname{Fun}'( \widehat{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \lambda } ) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{E}}/ \operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \lambda } )$ of inner fibrations over $\operatorname{\mathcal{C}}$, so that $T$ is an equivalence of $\infty $-categories. To complete the proof, it will suffice to show that the functor $\widehat{h}$ is fully faithful. In other words, we can replace $U$ by $\widehat{U}$ (and $\kappa $ by the cardinal $\lambda $) and thereby reduce to proving Lemma 9.4.8.8 under the assumption that $U$ is a cocartesian fibration. In this case, the desired result follows from Lemma 9.4.8.7 (and Remark 9.4.1.14). $\square$