Theorem 9.4.2.1. Let $\mathbb {K}$ be a collection of simplicial sets and let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of simplicial sets. Then a commutative diagram
9.35
\begin{equation} \begin{gathered}\label{equation:fiberwise-cocompletion-cocartesian-case} \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}}& } \end{gathered} \end{equation}
exhibits $\widehat{\operatorname{\mathcal{E}}}$ as a fiberwise $\mathbb {K}$-cocompletion of $\operatorname{\mathcal{E}}$ if and only if the following conditions are satisfied:
- $(a)$
For each vertex $C \in \operatorname{\mathcal{C}}$, the functor $H_{C}: \operatorname{\mathcal{E}}_{C} \rightarrow \widehat{\operatorname{\mathcal{E}}}_{C}$ exhibits the $\infty $-category $\widehat{\operatorname{\mathcal{E}}}_{C}$ as a $\mathbb {K}$-cocompletion of the $\infty $-category $\operatorname{\mathcal{E}}_{C}$ (Definition 8.4.5.1).
- $(b)$
The morphism $\widehat{U}$ is a cocartesian fibration of simplicial sets.
- $(c)$
For every edge $f: C \rightarrow C'$ of $\operatorname{\mathcal{C}}$, the covariant transport functor $f_{!}: \widehat{\operatorname{\mathcal{E}}}_{C} \rightarrow \widehat{\operatorname{\mathcal{E}}}_{C'}$ preserves $K$-indexed colimits for each $K \in \mathbb {K}$.
- $(d)$
The morphism $H$ carries $U$-cocartesian edges of $\operatorname{\mathcal{E}}$ to $\widehat{U}$-cocartesian edges of $\widehat{\operatorname{\mathcal{E}}}$.
Moreover, there exists a diagram (9.35) which satisfies these conditions.
Proof of Theorem 9.4.2.1.
Let $\mathbb {K}$ be a collection of simplicial sets and let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of simplicial sets. Using Lemma 9.4.2.6, we can choose a commutative diagram
9.39
\begin{equation} \begin{gathered}\label{equation:proof-of-fiberwise-cocompletion} \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}}& } \end{gathered} \end{equation}
which satisfies conditions $(a)$, $(b)$, $(c)$, and $(d)$ of Theorem 9.4.2.1. Lemma 9.4.2.3 guarantees any such diagram (9.39) exhibits $\widehat{\operatorname{\mathcal{E}}}$ as a fiberwise $\mathbb {K}$-cocompletion of $\operatorname{\mathcal{E}}$. Conversely, if we are given another diagram
9.40
\begin{equation} \begin{gathered}\label{equation:proof-of-fiberwise-cocompletion2} \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}}& } \end{gathered} \end{equation}
which exhibits $\widehat{\operatorname{\mathcal{E}}}'$ as a fiberwise $\mathbb {K}$-cocompletion of $\operatorname{\mathcal{E}}$, then Remark 9.4.1.21 guarantees that there is an equivalence $F: \widehat{\operatorname{\mathcal{E}}} \rightarrow \widehat{\operatorname{\mathcal{E}}}'$ of inner fibrations over $\operatorname{\mathcal{C}}$ such that $H'$ is isomorphic to $F \circ H$ as an object of $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}, \widehat{\operatorname{\mathcal{E}}}' )$. It then follows that (9.40) also satisfies conditions $(a)$, $(b)$, $(c)$, and $(d)$ of Theorem 9.4.2.1.
$\square$