# Kerodon

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

Example 5.2.2.12. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of simplicial sets, let $f: C \rightarrow D$ be an edge of $\operatorname{\mathcal{C}}$, let $\operatorname{\mathcal{E}}_{C} = \{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$ and $\operatorname{\mathcal{E}}_{D} = \{ D\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$ denote the corresponding fibers of $U$. Suppose we are given a commutative diagram of simplicial sets

$\xymatrix@R =50pt@C=50pt{ \Delta ^1 \times \operatorname{\mathcal{E}}_{C} \ar [r]^-{\widetilde{F}} \ar [d] & \operatorname{\mathcal{E}}\ar [d]^{U} \\ \Delta ^1 \ar [r]^-{f} & \operatorname{\mathcal{C}}, }$

where the restriction $\widetilde{F}|_{ \{ 0\} \times \operatorname{\mathcal{E}}_{C} }$ is the identity map from $\operatorname{\mathcal{E}}_{C}$ to itself, and set $F = \widetilde{F}|_{ \{ 1\} \times \operatorname{\mathcal{E}}_{C} } \in \operatorname{Fun}( \operatorname{\mathcal{E}}_{C}, \operatorname{\mathcal{E}}_{D} )$. Then $\widetilde{F}$ witnesses $F$ as given by covariant transport along $f$ (in the sense of Definition 5.2.2.4) if and only if it is a $U$-cocartesian lift of $U \circ \widetilde{F}$ (in the sense of Definition 5.2.2.10).