Lemma 11.9.7.3. Let $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{QC}}$ be a diagram and let $X$ be a simplicial set. Then the comparison map
\[ \theta : \int _{\operatorname{\mathcal{C}}} \mathscr {F}^{X} \rightarrow \operatorname{\mathcal{C}}\times _{ \operatorname{Fun}(X, \operatorname{\mathcal{C}}) } \operatorname{Fun}(X, \int _{\operatorname{\mathcal{C}}} \mathscr {F} ) \]
of Construction 11.9.7.2 is an equivalence of cocartesian fibrations over $\operatorname{\mathcal{C}}$.
Proof.
Let $U: \int _{\operatorname{\mathcal{C}}} \mathscr {F}^{X} \rightarrow \operatorname{\mathcal{C}}$ and $V: \operatorname{\mathcal{C}}\times _{ \operatorname{Fun}(X, \operatorname{\mathcal{C}}) } \operatorname{Fun}(X, \int _{\operatorname{\mathcal{C}}} \mathscr {F} ) \rightarrow \operatorname{\mathcal{C}}$ be the projection maps. By virtue of Proposition 5.1.7.15, it will suffice to prove the following:
- $(1)$
For every vertex $C \in \operatorname{\mathcal{C}}$, the map of fibers
\[ \theta _{C}: \{ C\} \times _{\operatorname{\mathcal{C}}} \int _{\operatorname{\mathcal{C}}} \mathscr {F}^{X} \rightarrow \{ C\} \times _{ \operatorname{Fun}(X, \operatorname{\mathcal{C}}) } \operatorname{Fun}(X, \int _{\operatorname{\mathcal{C}}} \mathscr {F} ) \]
is an equivalence of $\infty $-categories.
- $(2)$
The morphism $\theta $ carries carries $U$-cocartesian edges of $\int _{\operatorname{\mathcal{C}}} \mathscr {F}^{X}$ to $V$-cocartesian edges of $\operatorname{\mathcal{C}}\times _{ \operatorname{Fun}(X,\operatorname{\mathcal{C}})} \operatorname{Fun}(X, \int _{\operatorname{\mathcal{C}}}( \mathscr {F} ))$.
We first prove $(2)$. By virtue of Remark 5.1.1.12 and Theorem 5.2.1.1, it will suffice to show that for each vertex $x \in X$, the evaluation map $\mathscr {F}^{X} \rightarrow \mathscr {F}^{\{ x\} } \simeq \mathscr {F}$ carries $U$-cocartesian edges of $\int _{\operatorname{\mathcal{C}}} \mathscr {F}^{X}$ to $U'$-cocartesian edges of $\int _{\operatorname{\mathcal{C}}} \mathscr {F}$, where $U': \int _{\operatorname{\mathcal{C}}} \mathscr {F} \rightarrow \operatorname{\mathcal{C}}$ is the projection map. This follows immediately from Remark 11.9.7.1.
To prove $(1)$, we can assume without loss of generality that $\operatorname{\mathcal{C}}= \Delta ^{0}$ is a $0$-simplex, in which case the diagram $\mathscr {F}: \Delta ^{0} \rightarrow \operatorname{\mathcal{QC}}$ correponds to an $\infty $-category $\operatorname{\mathcal{E}}$ and $\theta $ corresponds to a functor of $\infty $-categories from $\int _{\Delta ^{0}} \operatorname{Fun}(X, \operatorname{\mathcal{E}})$ to $\operatorname{Fun}(X, \int _{\Delta ^{0}} \operatorname{\mathcal{E}})$. Let $\theta _{\operatorname{\mathcal{E}}}: \operatorname{\mathcal{E}}\rightarrow \int _{\Delta ^{0}} \operatorname{\mathcal{E}}$ and $\rho _{ \operatorname{Fun}(X,\operatorname{\mathcal{E}})}: \operatorname{Fun}(X, \operatorname{\mathcal{E}}) \rightarrow \int _{ \Delta ^{0} } \operatorname{Fun}(X, \operatorname{\mathcal{E}})$ be the comparison maps described in Example 5.6.2.17. Unwinding the definitions, we see that the composition
\[ \operatorname{Fun}(X, \operatorname{\mathcal{E}}) \xrightarrow {\rho _{\operatorname{Fun}(X,\operatorname{\mathcal{E}})}} \int _{ \Delta ^{0} } \operatorname{Fun}(X, \operatorname{\mathcal{E}}) \xrightarrow { \theta } \operatorname{Fun}(X, \int _{\Delta ^{0}} \operatorname{\mathcal{E}}) \]
coincides with the map given by postcomposition with $\rho _{\operatorname{\mathcal{E}}}$. It follows from Example 5.6.2.17 that $\rho _{\operatorname{Fun}(X, \operatorname{\mathcal{E}})}$ and $\theta \circ \rho _{ \operatorname{Fun}(X, \operatorname{\mathcal{E}})}$ are equivalences of $\infty $-categories, so that $\theta $ is also an equivalence of $\infty $-categories (Remark 4.5.1.18).
$\square$