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

Corollary Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of $\infty $-categories, let $U': \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{C}}$ be a left fibration of $\infty $-categories, and let $X$ be an initial object of $\operatorname{\mathcal{E}}'$. Then evaluation at $X$ induces a trivial Kan fibration of $\infty $-categories

\[ \operatorname{ev}_{X}: \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{E}}) \rightarrow \{ X\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}. \]

Proof. By virtue of Remark, we can replace $U$ by the projection map $\operatorname{\mathcal{E}}' \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{E}}'$ and thereby reduce to the case where $U'$ is the identity map. In this case, the desired result follows from Proposition, since the inclusion map $\{ X\} \hookrightarrow \operatorname{\mathcal{E}}'$ is left anodyne (Corollary $\square$