Kerodon

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

Example 7.7.2.5. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cartesian fibration of simplicial sets and let $F: K^{\triangleright } \rightarrow \operatorname{\mathcal{C}}$ be a diagram, carrying the cone point of $K^{\triangleright }$ to a vertex $C \in \operatorname{\mathcal{C}}$. Then evaluation at the cone point of $K^{\triangleright }$ induces a trivial Kan fibration $\operatorname{Fun}^{\operatorname{ACart}}_{/\operatorname{\mathcal{C}}}(K^{\triangleright }, \operatorname{\mathcal{E}}) \rightarrow \operatorname{\mathcal{E}}_{C}$. See Proposition 5.3.1.21.