Kerodon

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

Definition 5.2.2.1. 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 the simplicial set $\operatorname{\mathcal{C}}$, and let $F: \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{D}$ be a functor. We say that $F$ is given by covariant transport along $f$ if there exists a morphism of simplicial sets $\widetilde{f}: \Delta ^1 \times \operatorname{\mathcal{C}}_{X} \rightarrow \operatorname{\mathcal{C}}$ which satisfies the following conditions:

$(1)$

The diagram of simplicial sets

\[ \xymatrix@R =50pt@C=50pt{ \Delta ^1 \times \operatorname{\mathcal{C}}_{X} \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 equal to the identity functor $\operatorname{id}_{\operatorname{\mathcal{E}}_{C}}$, and the restriction $h|_{ \{ 1\} \times \operatorname{\mathcal{E}}_{C} \} }$ is equal to the functor $F$.

$(3)$

For each object $X$ of the $\infty $-category $\operatorname{\mathcal{E}}_{C}$, the restriction $h|_{ \Delta ^1 \times \{ X\} }$ is a locally $U$-cocartesian edge of $\operatorname{\mathcal{E}}$.

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