Lemma 9.4.4.4. Let $\mathbb {K}$ be a collection of simplicial sets, let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be an inner fibration of simplicial sets, and let $\operatorname{\mathcal{C}}_0 \subseteq \operatorname{\mathcal{C}}$ be a simplicial subset. Set $\operatorname{\mathcal{E}}_0 = \operatorname{\mathcal{C}}_0 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}$, let $U_0: \operatorname{\mathcal{E}}_0 \rightarrow \operatorname{\mathcal{C}}_0$ be the projection onto the first factor, and suppose we are given a diagram
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}_0 \ar [rr]^-{H_0} \ar [dr]_{ U_0 } & & \widehat{\operatorname{\mathcal{E}}}_0 \ar [dl]^{ \widehat{U}_0 } \\ & \operatorname{\mathcal{C}}_0 & } \]
which exhibits $\widehat{\operatorname{\mathcal{E}}}_0$ as a fiberwise $\mathbb {K}$-cocompletion of $\operatorname{\mathcal{E}}_0$. Then there exists a diagram
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}\ar [rr]^-{H} \ar [dr]_{ U } & & \widehat{\operatorname{\mathcal{E}}} \ar [dl]^{ \widehat{U}} \\ & \operatorname{\mathcal{C}}& } \]
which exhibits $\widehat{\operatorname{\mathcal{E}}}$ as a fiberwise cocompletion of $\operatorname{\mathcal{E}}$ and an isomorphism $\widehat{\operatorname{\mathcal{E}}}_0 \simeq \operatorname{\mathcal{C}}_0 \times _{\operatorname{\mathcal{C}}} \widehat{\operatorname{\mathcal{E}}}$ which carries $H_0$ to the map $(U_0, H): \operatorname{\mathcal{E}}_0 \rightarrow \operatorname{\mathcal{C}}_0 \times _{\operatorname{\mathcal{C}}} \widehat{\operatorname{\mathcal{E}}}$.
Proof.
Using Proposition 1.1.4.12, we can reduce to the case where $\operatorname{\mathcal{C}}= \Delta ^ n$ is a standard simplex and $\operatorname{\mathcal{C}}_0 = \operatorname{\partial \Delta }^ n$ is its boundary. In this case, $U$ is an isofibration of $\infty $-categories (Example 4.4.1.6). Applying Lemma 9.4.4.3, we deduce that there exists a diagram
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}\ar [rr]^-{H'} \ar [dr]_{ U } & & \widehat{\operatorname{\mathcal{E}}}' \ar [dl]^{ \widehat{U}'} \\ & \operatorname{\mathcal{C}}& } \]
which exhibits $\widehat{\operatorname{\mathcal{E}}}'$ as a fiberwise $\mathbb {K}$-cocompletion of $\operatorname{\mathcal{E}}$. Set $\widehat{\operatorname{\mathcal{E}}}'_0 = \operatorname{\mathcal{C}}_0 \times _{\operatorname{\mathcal{C}}} \widehat{\operatorname{\mathcal{E}}}$, so that $H'_0 = H'|_{\operatorname{\mathcal{E}}_0}$ exhibits $\widehat{\operatorname{\mathcal{E}}}'_0$ as a fiberwise $\mathbb {K}$-completion of $\operatorname{\mathcal{E}}_0$. Applying Remark 9.4.1.21, we deduce that there exists an isomorphism $H'_0 \simeq F_0 \circ H_0$ in the $\infty $-category $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}_0 }( \operatorname{\mathcal{E}}_0, \widehat{\operatorname{\mathcal{E}}}'_0 )$, where $F_0: \widehat{\operatorname{\mathcal{E}}}_0 \rightarrow \widehat{\operatorname{\mathcal{E}}}'_0$ is an equivalence of inner fibrations over $\operatorname{\mathcal{C}}_0$. Using Lemma 5.6.7.1, we can choose an inner fibration $\widehat{U}: \widehat{\operatorname{\mathcal{E}}} \rightarrow \operatorname{\mathcal{C}}$ and an equivalence $F: \widehat{\operatorname{\mathcal{E}}} \rightarrow \widehat{\operatorname{\mathcal{E}}}'$ satisfying $F_0 = F|_{\widehat{\operatorname{\mathcal{E}}}_0}$. Composition with $F$ induces an equivalence of $\infty $-categories $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}, \widehat{\operatorname{\mathcal{E}}} ) \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}, \widehat{\operatorname{\mathcal{E}}}' )$. We can therefore choose a functor $H: \operatorname{\mathcal{E}}\rightarrow \widehat{\operatorname{\mathcal{E}}}$ such that $F \circ H$ is isomorphic to $H'$ in the $\infty $-category $\operatorname{Fun}_{/\operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}, \widehat{\operatorname{\mathcal{E}}}' )$. It follows that $F_0 \circ H|_{ \operatorname{\mathcal{E}}_0 }$ is isomorphic to $F_0 \circ H_0$ as objects of the $\infty $-category $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}_0 }( \operatorname{\mathcal{E}}_0, \widehat{\operatorname{\mathcal{E}}}'_0 )$. Since $F_0$ is an equivalence of inner fibrations over $\operatorname{\mathcal{C}}_0$, it follows that $H_0$ and $H|_{\operatorname{\mathcal{E}}_0}$ are isomorphic as objects of the $\infty $-category $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}_0 }( \operatorname{\mathcal{E}}_0, \widehat{\operatorname{\mathcal{E}}}_0 )$. Since the restriction functor $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}, \widehat{\operatorname{\mathcal{E}}} ) \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{C}}_0 }( \operatorname{\mathcal{E}}_0, \widehat{\operatorname{\mathcal{E}}}_0 )$ is an isofibration (Proposition 4.1.4.1), we can arrange (after replacing $H$ by an isomorphic functor if necessary) that $H|_{\operatorname{\mathcal{E}}_0} = H_0$. We conclude by observing that the diagram
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}\ar [rr]^-{H} \ar [dr]_{ U } & & \widehat{\operatorname{\mathcal{E}}} \ar [dl]^{ \widehat{U}} \\ & \operatorname{\mathcal{C}}& } \]
exhibits $\widehat{\operatorname{\mathcal{E}}}$ as a fiberwise $\mathbb {K}$-cocompletion of $\operatorname{\mathcal{E}}$.
$\square$