Theorem 9.4.1.20. Let $\mathbb {K}$ be a collection of simplicial sets. Suppose we are given a diagram of simplicial sets
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}\ar [dr]_{ U } \ar [rr]^-{H} & & \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}}$. Then, for every $\mathbb {K}$-cocomplete inner fibration $U': \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{C}}$, precomposition with $H$ induces an equivalence of $\infty $-categories
\[ \operatorname{Fun}^{\mathbb {K}}_{ / \operatorname{\mathcal{C}}}( \widehat{\operatorname{\mathcal{E}}}, \operatorname{\mathcal{E}}' ) \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}(\operatorname{\mathcal{E}}, \operatorname{\mathcal{E}}'). \]
Proof of Theorem 9.4.1.20.
For every morphism of simplicial sets $S \rightarrow \operatorname{\mathcal{C}}$, we let $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\mathbb {K}}( S \times _{\operatorname{\mathcal{C}}} \widehat{\operatorname{\mathcal{E}}}, \operatorname{\mathcal{E}}' )$ denote the (replete) full subcategory of $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( S \times _{\operatorname{\mathcal{C}}} \widehat{\operatorname{\mathcal{E}}}, \operatorname{\mathcal{E}}' )$ spanned by those morphisms $F: S \times _{\operatorname{\mathcal{C}}} \widehat{\operatorname{\mathcal{E}}} \rightarrow \operatorname{\mathcal{E}}'$ having the property that, for each vertex $s \in S$, the functor $F_{s}: \{ s\} \times _{\operatorname{\mathcal{C}}} \widehat{\operatorname{\mathcal{E}}} \rightarrow \{ s\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}'$ preserves $K$-indexed colimits for each $K \in \mathbb {K}$. We will prove the following:
- $(\ast )$
For every morphism of simplicial sets $S \rightarrow \operatorname{\mathcal{C}}$, precomposition with $H$ induces an equivalence of $\infty $-categories
\[ \theta _{S}: \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\mathbb {K}}( S \times _{\operatorname{\mathcal{C}}} \widehat{\operatorname{\mathcal{E}}}, \operatorname{\mathcal{E}}' ) \rightarrow \operatorname{Fun}_{/\operatorname{\mathcal{C}}}( S \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}, \operatorname{\mathcal{E}}' ). \]
Writing $S$ as the union of its skeleta $\operatorname{sk}_{n}(S)$, we can realize $\theta _{S}$ as the limit of a tower of comparison maps
\[ \xymatrix@R =50pt@C=50pt{ \cdots \ar [r] & \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\mathbb {K}}( \operatorname{sk}_1(S) \times _{\operatorname{\mathcal{C}}} \widehat{\operatorname{\mathcal{E}}}, \operatorname{\mathcal{E}}' ) \ar [d]^{ \theta _{ \operatorname{sk}_1(S) }} \ar [r] & \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\mathbb {K}}( \operatorname{sk}_0(S) \times _{\operatorname{\mathcal{C}}} \widehat{\operatorname{\mathcal{E}}}, \operatorname{\mathcal{E}}' ) \ar [d]^{ \theta _{ \operatorname{sk}_0(S) }} \\ \cdots \ar [r] & \operatorname{Fun}_{/\operatorname{\mathcal{C}}}( \operatorname{sk}_1(S) \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}, \operatorname{\mathcal{E}}' ) \ar [r] & \operatorname{Fun}_{/\operatorname{\mathcal{C}}}( \operatorname{sk}_0(S) \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}, \operatorname{\mathcal{E}}' ), } \]
where the horizontal maps are isofibrations (Variant 4.4.5.11). Consequently, to show that $\theta _{S}$ is an equivalence of $\infty $-categories, it will suffice to show that $\theta _{ \operatorname{sk}_ n(S) }$ is an equivalence of $\infty $-categories for each $n \geq -1$. We may therefore assume without loss of generality that $S$ has dimension $\leq n$, for some integer $n \geq -1$.
We now proceed by induction on $n$. Assume that $n \geq 0$ (otherwise, $S$ is empty and there is nothing to prove). Let $S'$ be the $(n-1)$-skeleton of $S$, so that Proposition 1.1.4.12 supplies a pushout diagram
\[ \xymatrix@R =50pt@C=50pt{ T' \ar [r] \ar [d] & T \ar [d] \\ S' \ar [r] & S } \]
where $T$ is a coproduct of standard $n$-simplices (indexed by the nondegenerate $n$-simplices of $S$) and $T'$ is the coproduct of their boundaries. It follows that $\theta _{S}$ can be realized as the horizontal limit of a diagram of comparison maps
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\mathbb {K}}( S' \times _{\operatorname{\mathcal{C}}} \widehat{\operatorname{\mathcal{E}}}, \operatorname{\mathcal{E}}' ) \ar [d]^{\theta _{S'}} \ar [r] & \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\mathbb {K}}( T' \times _{\operatorname{\mathcal{C}}} \widehat{\operatorname{\mathcal{E}}}, \operatorname{\mathcal{E}}' ) \ar [d]^{ \theta _{T'} } \ar [r] & \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\mathbb {K}}( T \times _{\operatorname{\mathcal{C}}} \widehat{\operatorname{\mathcal{E}}}, \operatorname{\mathcal{E}}' ) \ar [d]^{\theta _{T}} \\ \operatorname{Fun}_{/\operatorname{\mathcal{C}}}( S' \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}, \operatorname{\mathcal{E}}' ) \ar [r] & \operatorname{Fun}_{/\operatorname{\mathcal{C}}}( T' \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}, \operatorname{\mathcal{E}}' ) & \operatorname{Fun}_{/\operatorname{\mathcal{C}}}( T \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}, \operatorname{\mathcal{E}}' ), \ar [l] } \]
where the horizontal maps on the right are isofibrations (Variant 4.4.5.11). Since the simplicial sets $S'$ and $T'$ have dimension $< n$, our inductive hypothesis guarantees that $\theta _{S'}$ and $\theta _{T'}$ are equivalences of $\infty $-categories. Consequently, to show that $\theta _{S}$ is an equivalence of $\infty $-categories, it will suffice to show that $\theta _{T}$ is an equivalence of $\infty $-categories (Corollary 4.5.2.30). Replacing $\operatorname{\mathcal{C}}$ by $T$, we are reduced to proving Theorem 9.4.1.20 in the special case where $\operatorname{\mathcal{C}}$ is a coproduct of standard simplices. In this case, $\operatorname{\mathcal{C}}$ is an $\infty $-category and the inner fibrations $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$, $\widehat{U}: \widehat{\operatorname{\mathcal{E}}} \rightarrow \operatorname{\mathcal{C}}$, and $U': \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{C}}$ are automatically isofibrations (Example 4.4.1.6), so the desired result follows from Lemma 9.4.1.27.
$\square$