Kerodon

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

Corollary 7.3.6.10. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category containing an initial object $C$, let $U: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{E}}$ be a cocartesian fibration of $\infty $-categories, and let $F,G: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be a pair of functors satisfying $U \circ F = U \circ G$. Suppose that $F$ carries each morphism of $\operatorname{\mathcal{C}}$ to a $U$-cocartesian morphism of $\operatorname{\mathcal{D}}$. Then evaluation at $C$ induces a homotopy equivalence

\[ \theta : \operatorname{Hom}_{ \operatorname{Fun}_{ /\operatorname{\mathcal{E}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}) }( F, G ) \rightarrow \operatorname{Hom}_{ \operatorname{Fun}_{/\operatorname{\mathcal{E}}}( \{ C\} , \operatorname{\mathcal{D}}) }( F(C), G(C)). \]

Proof. Let $\operatorname{\mathcal{C}}^{\mathrm{init}}$ denote the full subcategory of $\operatorname{\mathcal{C}}$ spanned by its initial objects. The morphism $\theta $ then factors as a composition

\begin{eqnarray*} \operatorname{Hom}_{ \operatorname{Fun}_{ /\operatorname{\mathcal{E}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}) }( F, G ) & \xrightarrow {\theta '} & \operatorname{Hom}_{ \operatorname{Fun}_{ /\operatorname{\mathcal{E}}}( \operatorname{\mathcal{C}}^{\mathrm{init}}, \operatorname{\mathcal{D}}) }( F|_{\operatorname{\mathcal{C}}^{\mathrm{init}}}, G|_{ \operatorname{\mathcal{C}}^{\mathrm{init}}} ) \\ & \xrightarrow {\theta ''} & \operatorname{Hom}_{ \operatorname{Fun}_{/\operatorname{\mathcal{E}}}( \{ C\} , \operatorname{\mathcal{D}}) }( F(C), G(C)). \end{eqnarray*}

Our assumption guarantees that $F$ is $U$-left Kan extended from $\operatorname{\mathcal{C}}^{\mathrm{init}}$ (Corollary 7.3.3.13), so that the morphism $\theta '$ is a homotopy equivalence (Proposition 7.3.6.7). Since $\operatorname{\mathcal{C}}^{\mathrm{init}}$ is a contractible Kan complex (Corollary 4.6.7.14), the inclusion map $\{ C\} \hookrightarrow \operatorname{\mathcal{C}}^{\mathrm{init}}$ is a categorical equivalence of simplicial sets, which implies that $\theta ''$ is also a homotopy equivalence. $\square$