Lemma 9.4.6.13. Let $\kappa $ be an uncountable regular cardinal, let $\operatorname{\mathcal{E}}$ be an $\infty $-category which is essentially $\kappa $-small, and suppose we are given a commutative diagram of $\infty $-categories
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}\ar [rr]^-{H} \ar [dr]_{U} & & \widehat{\operatorname{\mathcal{E}}} \ar [dl]^{ \widehat{U} } \\ & \Delta ^2 & } \]
which exhibits $\widehat{E}$ as a fiberwise $\kappa $-cocompletion of $\operatorname{\mathcal{E}}$. The following conditions are equivalent:
- $(1)$
The inclusion map $\Lambda ^{2}_{1} \times _{\Delta ^2} \operatorname{\mathcal{E}}\hookrightarrow \operatorname{\mathcal{E}}$ is a categorical equivalence of simplicial sets.
- $(2)$
The functor $\widehat{U}$ is a cartesian fibration.
Proof.
The implication $(2) \Rightarrow (1)$ follows from Lemma 9.4.6.12 and Corollary 9.4.5.9. Conversely, suppose that condition $(1)$ is satisfied. Set $\operatorname{\mathcal{E}}_0 = \Lambda ^{2}_{1} \times _{\Delta ^2} \operatorname{\mathcal{E}}$ and $\widehat{\operatorname{\mathcal{E}}}_0 = \Lambda ^{2}_{1} \times _{\Delta ^2} \widehat{\operatorname{\mathcal{E}}}$. Using Proposition 5.6.7.2, we can choose a pullback diagram
\[ \xymatrix@R =50pt@C=50pt{ \widehat{\operatorname{\mathcal{E}}}_0 \ar [d]^{ \widehat{U}_0 } \ar [r] & \widehat{\operatorname{\mathcal{E}}}' \ar [d]^{ \widehat{U}' } \\ \Lambda ^{2}_{1} \ar [r] & \Delta ^2, } \]
where $\widehat{U}'$ is a cartesian fibration. Let us abuse notation by identifying $\widehat{\operatorname{\mathcal{E}}}_0$ with its image in $\widehat{\operatorname{\mathcal{E}}}'$. It follows from Proposition 5.3.6.1 that the inclusion map $\widehat{\operatorname{\mathcal{E}}}_0 \hookrightarrow \widehat{\operatorname{\mathcal{E}}}'$ is a categorical equivalence of simplicial sets, so there exists a functor $F: \widehat{\operatorname{\mathcal{E}}}' \rightarrow \widehat{\operatorname{\mathcal{E}}}$ which is the identity on $\widehat{\operatorname{\mathcal{E}}}_0$. We will complete the proof by showing that $F$ is an equivalence of inner fibrations over $\Delta ^2$, so that $\widehat{U}$ is also a cartesian fibration (Proposition 5.1.7.14).
Note that the inner $\widehat{U}$ and $\widehat{U}'$ are $\kappa $-cocomplete. It will therefore suffice to show that, for every $\kappa $-cocomplete inner fibration $V: \operatorname{\mathcal{D}}\rightarrow \Delta ^2$, precomposition with $F$ induces an equivalence of $\infty $-categories
\[ \operatorname{Fun}^{\kappa }_{ / \Delta ^2 }( \widehat{\operatorname{\mathcal{E}}}, \operatorname{\mathcal{D}}) \rightarrow \operatorname{Fun}^{\kappa }_{ / \Delta ^2 }( \widehat{\operatorname{\mathcal{E}}}', \operatorname{\mathcal{D}}). \]
Since the inclusion $\widehat{\operatorname{\mathcal{E}}}_0 \hookrightarrow \widehat{\operatorname{\mathcal{E}}}'$ is a categorical equivalence, this is equivalent to the statement that the restriction map
\[ \operatorname{Fun}^{\kappa }_{ / \Delta ^2 }( \widehat{\operatorname{\mathcal{E}}}, \operatorname{\mathcal{D}}) \rightarrow \operatorname{Fun}^{\kappa }_{ / \Lambda ^2_1}( \widehat{\operatorname{\mathcal{E}}}_0, \operatorname{\mathcal{D}}_0 ) \]
is an equivalence, where $\operatorname{\mathcal{D}}_0 = \Lambda ^{2}_{1} \times _{\Delta ^2} \operatorname{\mathcal{D}}$. Invoking the universal property of fiberwise cocompletion (Theorem 9.4.1.20), we are reduced to showing that the restriction map $\operatorname{Fun}_{ / \Delta ^2 }( \operatorname{\mathcal{E}}, \operatorname{\mathcal{D}}) \rightarrow \operatorname{Fun}_{ / \Delta ^2 }( \Lambda ^{2}_{1} \times _{\Delta ^2}, \operatorname{\mathcal{E}}, \operatorname{\mathcal{D}})$ is an equivalence of $\infty $-categories, which follows immediately from assumption $(1)$.
$\square$