$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Lemma 9.4.1.27. Let $\mathbb {K}$ be a collection of simplicial sets. Suppose we are given a diagram of $\infty $-categories
\[ \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}}, & } \]
where $U$ and $\widehat{U}$ are isofibrations and $H$ exhibits $\widehat{\operatorname{\mathcal{E}}}$ as a fiberwise $\mathbb {K}$-cocompletion of $\operatorname{\mathcal{E}}$. Then, for every $\mathbb {K}$-cocomplete isofibration $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.
Since the functor $H$ is fully faithful (see Variant 4.8.6.19), we can assume without loss of generality that $\operatorname{\mathcal{E}}$ is a replete full subcategory of $\widehat{\operatorname{\mathcal{E}}}$ (and that $H$ is the inclusion functor). In this case, Proposition 9.4.1.25 identifies $\operatorname{Fun}^{\mathbb {K}}_{ / \operatorname{\mathcal{C}}}( \widehat{\operatorname{\mathcal{E}}}, \operatorname{\mathcal{E}}' )$ with the full subcategory of $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \widehat{\operatorname{\mathcal{E}}}, \operatorname{\mathcal{E}}' )$ spanned by those functors $F: \widehat{\operatorname{\mathcal{E}}} \rightarrow \operatorname{\mathcal{E}}'$ which are $U'$-left Kan extended from $\operatorname{\mathcal{E}}$. Combining this observation with Theorem 7.3.6.14 and Variant 9.4.1.26, we see that the restriction functor $\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}}')$ is a trivial Kan fibration.
$\square$