Proposition 5.2.2.17. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cartesian 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}}_{D} \rightarrow \operatorname{\mathcal{E}}_{C}$ which is given by contravariant transport along $f$.
An arbitrary functor $F': \operatorname{\mathcal{E}}_{D} \rightarrow \operatorname{\mathcal{E}}_{C}$ is given by contravariant transport along $f$ if and only if it is isomorphic to $F$ (as an object of the $\infty $-category $\operatorname{Fun}( \operatorname{\mathcal{E}}_{D}, \operatorname{\mathcal{E}}_{C} )$).