# Kerodon

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

Definition 5.2.2.4. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be an inner fibration of simplicial sets, let $f: C \rightarrow D$ be an edge of $\operatorname{\mathcal{C}}$, and 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$. We will say that a functor $F: \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{D}$ is given by covariant transport along $f$ if there exists a morphism of simplicial sets $\widetilde{F}: \Delta ^1 \times \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}$ satisfying the following conditions:

$(1)$

The 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}}}$

commutes.

$(2)$

The restriction $\widetilde{F}|_{ \{ 0\} \times \operatorname{\mathcal{E}}_{C} }$ is the identity map $\operatorname{id}_{\operatorname{\mathcal{E}}_{C}}$, and the restriction $\widetilde{F}|_{ \{ 1\} \times \operatorname{\mathcal{E}}_{C} }$ is equal to $F$.

$(3)$

For every object $X$ of the $\infty$-category $\operatorname{\mathcal{E}}_ C$, the composite map

$\Delta ^1 \times \{ X\} \hookrightarrow \Delta ^1 \times \operatorname{\mathcal{E}}_{C} \xrightarrow { \widetilde{F} } \operatorname{\mathcal{E}}$

is a locally $U$-cocartesian edge of the simplicial set $\operatorname{\mathcal{E}}$.

If these conditions are satisfied, we say that the morphism $\widetilde{F}$ witnesses $F$ as given by covariant transport along $f$.