$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Corollary 9.4.3.4. Let $\mathbb {K}$ be a collection of simplicial sets and let $U^{\dagger }: \operatorname{\mathcal{E}}^{\dagger } \rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}}$ be a cartesian fibration of simplicial sets. Then there exists a diagram
9.44
\begin{equation} \begin{gathered}\label{equation:fiberwise-completion-cocartesian-case-revisited} \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}^{\dagger } \ar [rr]^-{H^{\dagger } } \ar [dr]_{U^{\dagger } } & & \widehat{\operatorname{\mathcal{E}}}^{\dagger } \ar [dl]^{ \widehat{U}^{\dagger } } \\ & \operatorname{\mathcal{C}}^{\operatorname{op}} & } \end{gathered} \end{equation}
which satisfies the conditions of Theorem 9.4.3.1.
Proof.
Using Corollary 8.6.6.3, we can choose a cocartesian fibration $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ and a morphism $T: \operatorname{\mathcal{E}}^{\dagger } \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{E}}$ which exhibits $U^{\dagger }$ as a cartesian conjugate of $U$. Applying Theorem 9.4.2.1, we can choose 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}}$, where $\widehat{U}$ is a cocartesian fibration. Using Proposition 8.6.2.3, we can choose a cartesian fibration $\widehat{U}^{\dagger }: \widehat{\operatorname{\mathcal{E}}}^{\dagger } \rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}}$ and a morphism $\widehat{T}: \widehat{\operatorname{\mathcal{E}}}^{\dagger } \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \rightarrow \widehat{\operatorname{\mathcal{E}}}$ which exhibits $\widehat{U}^{\dagger }$ as a cartesian conjugate of $\widehat{U}$. The desired result now follows from Proposition 9.4.3.3.
$\square$