Corollary 8.4.7.2. Let $U: \widetilde{\operatorname{\mathcal{C}}} \rightarrow \operatorname{\mathcal{C}}$ be a right fibration between essentially small $\infty $-categories and let $\mathscr {F}: \operatorname{\mathcal{C}}^{\operatorname{op}} \rightarrow \operatorname{\mathcal{S}}$ be a covariant transport representation for the left fibration $U^{\operatorname{op}}$. Then there exists an equivalence of $\infty $-categories $T: \operatorname{Fun}( \widetilde{\operatorname{\mathcal{C}}}^{\operatorname{op}}, \operatorname{\mathcal{S}}) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{S}})_{ / \mathscr {F} }$ for which the diagram of $\infty $-categories
\[ \xymatrix@R =50pt@C=50pt{ \widetilde{\operatorname{\mathcal{C}}} \ar [dd]^{U} \ar [r]^-{ h_{\bullet }^{\widetilde{\operatorname{\mathcal{C}}}} }& \operatorname{Fun}( \widetilde{\operatorname{\mathcal{C}}}^{\operatorname{op}}, \operatorname{\mathcal{S}}) \ar [d]^{T} \\ & \operatorname{Fun}( \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{S}})_{ / \mathscr {F}} \ar [d] \\ \operatorname{\mathcal{C}}\ar [r]^-{ h_{\bullet }^{\operatorname{\mathcal{C}}}} & \operatorname{Fun}( \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{S}}) } \]
commutes up to isomorphism. Here $h_{\bullet }^{\operatorname{\mathcal{C}}}$ and $h_{\bullet }^{ \widetilde{\operatorname{\mathcal{C}}} }$ denote covariant Yoneda embeddings for $\operatorname{\mathcal{C}}$ and $\widetilde{\operatorname{\mathcal{C}}}$, respectively.
Proof.
Using Corollary 8.4.2.7, we can choose categorical pullback square
\[ \xymatrix@R =50pt@C=50pt{ \widetilde{\operatorname{\mathcal{C}}} \ar [r]^-{ \widetilde{h} } \ar [d]^{U} & \operatorname{Fun}( \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{S}})_{ / \mathscr {F} } \ar [d] \\ \operatorname{\mathcal{C}}\ar [r]^-{ h_{\bullet }^{\operatorname{\mathcal{C}}} } & \operatorname{Fun}( \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{S}}). } \]
It follows from Theorem 8.4.0.3 that the functor $\widetilde{h}$ factors (up to isomorphism) as a composition
\[ \widetilde{\operatorname{\mathcal{C}}} \xrightarrow { h_{\bullet }^{ \widetilde{\operatorname{\mathcal{C}}} } } \operatorname{Fun}( \widetilde{\operatorname{\mathcal{C}}}^{\operatorname{op}}, \operatorname{\mathcal{S}}) \xrightarrow {T} \operatorname{Fun}( \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{S}})_{ / \mathscr {F} }, \]
where the functor $T$ preserves small colimits. To complete the proof, it will suffice to show that $T$ is an equivalence of $\infty $-categories. This is equivalent to the assertion that $\widetilde{h}$ exhibits $\operatorname{Fun}( \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{S}})_{ / \mathscr {F} }$ as a cocompletion of $\widetilde{\operatorname{\mathcal{C}}}$, which is a special case of Proposition 8.4.7.1.
$\square$