Corollary 5.3.1.22 (035T)

Corollary 5.3.1.22. 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 5.3.1.13, 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 5.3.1.21, since the inclusion map $\{ X\} \hookrightarrow \operatorname{\mathcal{E}}'$ is left anodyne (Corollary 4.6.7.24). $\square$