Proposition 5.2.2.8 (01VS)

Proposition 5.2.2.8. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of simplicial sets and let $f: C \rightarrow D$ be an edge of $\operatorname{\mathcal{C}}$. Then:

There exists a functor $F: \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{D}$ which is given by covariant transport along $f$.
An arbitrary functor $F': \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{D}$ is given by covariant transport along $f$ if and only if it is isomorphic to $F$ (as an object of the $\infty $-category $\operatorname{Fun}(\operatorname{\mathcal{E}}_{C}, \operatorname{\mathcal{E}}_{D} )$).

Proof of Proposition 5.2.2.8. Apply Lemma 5.2.2.13 in the special case where $K$ is the $\infty $-category $\operatorname{\mathcal{E}}_{C}$, $H_0: K \rightarrow \operatorname{\mathcal{E}}$ is the inclusion map, and $\overline{H}$ is the composite map $\Delta ^1 \times K \rightarrow \Delta ^1 \xrightarrow {f} \operatorname{\mathcal{C}}$ (see Example 5.2.2.12). $\square$