$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Proposition 5.2.2.1. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of categories and let $f: C \rightarrow D$ be a morphism of $\operatorname{\mathcal{C}}$. For each object $X \in \operatorname{\mathcal{E}}_{C}$, let $\widetilde{f}_{X}$ be a $U$-cocartesian morphism of $\operatorname{\mathcal{E}}$ having source $X$ and satisfying $U( \widetilde{f}_{X} ) = f$. Then there is a unique functor $f_{!}: \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{D}$ with the following properties:
For each object $X \in \operatorname{\mathcal{E}}_{C}$, the object $f_{!}(X) \in \operatorname{\mathcal{E}}_{D}$ is the target of the morphism $\widetilde{f}_{X}$.
The construction $X \mapsto \widetilde{f}_{X}$ determines a natural transformation from the inclusion functor $\operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}$ to the functor $f_{!}: \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{D} \subseteq \operatorname{\mathcal{E}}$.
Proof.
For each object $X \in \operatorname{\mathcal{E}}_{C}$, let $f_{!}(X)$ denote the target of the morphism $\widetilde{f}_{X}$. Let $u: X \rightarrow Y$ be a morphism in the category $\operatorname{\mathcal{E}}_{C}$. Invoking our assumption that $\widetilde{f}_{X}$ is $U$-cocartesian, we see that there is a unique morphism $f_{!}(u): f_{!}(X) \rightarrow f_{!}(Y)$ for which the diagram
5.12
\begin{equation} \begin{gathered}\label{equation:defining-contravariant-transport} \xymatrix@R =50pt@C=50pt{ X \ar [d]^{u} \ar [r]^-{ \widetilde{f}_{X} } & f_{!}(X) \ar [d]^{ f_{!}(u) } \\ Y \ar [r]^-{ \widetilde{f}_{Y} } & f_{!}(Y) } \end{gathered} \end{equation}
is commutative (in the category $\operatorname{\mathcal{E}}$). Note that if $v: Y \rightarrow Z$ is another morphism in the category $\operatorname{\mathcal{E}}_{C}$, then the calculation
\[ f_{!}(v) \circ f_{!}(u) \circ \widetilde{f}_{X} = f_{!}(v) \circ \widetilde{f}_{Y} \circ u = \widetilde{f}_{Z} \circ v \circ u \]
shows that $f_{!}( v \circ u) = f_{!}(v) \circ f_{!}(u)$. Similarly, for each object $X \in \operatorname{\mathcal{E}}_{C}$, the calculation $\widetilde{f}_{X} \circ \operatorname{id}_{ f_{!}(X) } = \widetilde{f}_{X} = \operatorname{id}_{X} \circ \widetilde{f}_{X}$ shows that $f_{!}( \operatorname{id}_{X} ) = \operatorname{id}_{ f_{!}(X)}$. We can therefore regard $f_{!}$ as a functor from the category $\operatorname{\mathcal{E}}_{C}$ to $\operatorname{\mathcal{E}}_{D}$, and the commutativity of (5.12) guarantees that the construction $X \mapsto \widetilde{f}_{X}$ determines a natural transformation from the inclusion $\operatorname{\mathcal{E}}_{C} \hookrightarrow \operatorname{\mathcal{E}}$ to the functor $f_{!}$.
$\square$