Definition 5.2.2.14. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be an inner fibration of simplicial sets, let $C$ and $D$ be vertices of $\operatorname{\mathcal{C}}$, and let $f: C \rightarrow D$ be an edge of $\operatorname{\mathcal{C}}$. We say that a functor $F: \operatorname{\mathcal{E}}_{D} \rightarrow \operatorname{\mathcal{E}}_{C}$ is given by contravariant transport along $f$ if there exists a morphism of simplicial sets $\widetilde{F}: \Delta ^1 \times \operatorname{\mathcal{E}}_{D} \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}}_{D} \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}|_{ \{ 1\} \times \operatorname{\mathcal{E}}_{D}}$ is equal to the identity map $\operatorname{id}_{\operatorname{\mathcal{E}}_{D}}$, and the restriction $\widetilde{F}|_{ \{ 0\} \times \operatorname{\mathcal{E}}_{D}}$ is equal to $F$.
- $(3)$
For every object $Y$ of the $\infty $-category $\operatorname{\mathcal{E}}_{D}$, the composite map
\[ \Delta ^1 \times \{ Y\} \hookrightarrow \Delta ^1 \times \operatorname{\mathcal{E}}_ D \xrightarrow { \widetilde{F} } \operatorname{\mathcal{E}} \]is a locally $U$-cartesian 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 contravariant transport along $f$.