Corollary 5.3.1.23. Let $\overline{U}: \overline{\operatorname{\mathcal{E}}} \rightarrow \operatorname{\mathcal{C}}^{\triangleleft }$ be a cocartesian fibration of simplicial sets. Then evaluation at ${\bf 0}$ induces a trivial Kan fibration of simplicial sets
\[ \operatorname{Fun}_{/ \operatorname{\mathcal{C}}^{\triangleleft } }^{\operatorname{CCart}}( \operatorname{\mathcal{C}}^{\triangleleft }, \overline{\operatorname{\mathcal{E}}} ) \rightarrow \{ {\bf 0} \} \times _{ \operatorname{\mathcal{C}}^{\triangleleft } } \overline{\operatorname{\mathcal{E}}}. \]