# Kerodon

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

Definition 5.2.2.10. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of simplicial sets. Let $K$ be another simplicial set, let $H: \Delta ^1 \times K \rightarrow \operatorname{\mathcal{E}}$ be a morphism. We will say that $H$ is a $U$-cocartesian lift of $\overline{H} = U \circ H$ if, for every vertex $x \in K$, the restriction $H|_{ \Delta ^1 \times \{ x\} }$ is a $U$-cocartesian edge of $\operatorname{\mathcal{E}}$.