Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$ $\newcommand\empty{}$
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$

Corollary 11.5.0.25. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category, let $U: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{E}}$ be a functor of $\infty $-categories, and let $\operatorname{\mathcal{C}}^{0} \subseteq \operatorname{\mathcal{C}}$ be a full subcategory. Let $F,G: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be functors having restrictions $F_0 = F|_{\operatorname{\mathcal{C}}^{0}}$ and $G_0 = G|_{\operatorname{\mathcal{C}}^{0}}$, and suppose that $U \circ F = U \circ G$. If $F$ is $U$-left Kan extended from $\operatorname{\mathcal{C}}^{0}$ or $G$ is $U$-right Kan extended from $\operatorname{\mathcal{C}}^{0}$, then the restriction map

\[ \operatorname{Hom}_{ \operatorname{Fun}_{ /\operatorname{\mathcal{E}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}) }( F, G ) \rightarrow \operatorname{Hom}_{ \operatorname{Fun}_{ /\operatorname{\mathcal{E}}}( \operatorname{\mathcal{C}}^{0}, \operatorname{\mathcal{D}}) }( F_0, G_0 ) \]

is a homotopy equivalence of Kan complexes.