Proposition 5.3.6.9. Let $U: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{B}}$ be a cocartesian fibration of simplicial sets, let $f: B \rightarrow B'$ be an edge of $\operatorname{\mathcal{B}}$, and let $f_{!}: \operatorname{\mathcal{C}}_{B} \rightarrow \operatorname{\mathcal{C}}_{B'}$ be given by covariant transport along $f$ for the cocartesian fibration $U$ (see Definition 5.2.2.4). For every $\infty $-category $\operatorname{\mathcal{D}}$, the functor
\[ \operatorname{Fun}(\operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{D}})_{B'} \simeq \operatorname{Fun}( \operatorname{\mathcal{C}}_{B'}, \operatorname{\mathcal{D}}) \xrightarrow { \circ f_{!} } \operatorname{Fun}( \operatorname{\mathcal{C}}_{B}, \operatorname{\mathcal{D}}) \simeq \operatorname{Fun}(\operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{D}})_{B} \]
is given by contravariant transport along $f$ (for the cartesian fibration $\pi : \operatorname{Fun}(\operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{D}}) \rightarrow \operatorname{\mathcal{B}}$).
Proof.
Replacing $\operatorname{\mathcal{C}}$ by the fiber product $\Delta ^1 \times _{\operatorname{\mathcal{B}}} \operatorname{\mathcal{C}}$, we can assume without loss of generality that $\operatorname{\mathcal{B}}= \Delta ^1$ and $f$ is the nondegenerate edge of $\operatorname{\mathcal{B}}$. By virtue of Corollary 5.2.4.4, we can choose a functor $R: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}_{B'}$ such that $R|_{ \operatorname{\mathcal{C}}_{B} } = f_{!}$, $R|_{ \operatorname{\mathcal{C}}_{B'} } = \operatorname{id}$, and $R$ carries $U$-cocartesian morphisms of $\operatorname{\mathcal{C}}$ to isomorphisms in $\operatorname{\mathcal{C}}_{B'}$. Precomposition with functor $(U,R): \operatorname{\mathcal{C}}\rightarrow \Delta ^1 \times \operatorname{\mathcal{C}}_{B'}$ then determines a functor
\[ H: \Delta ^1 \times \operatorname{Fun}( \operatorname{\mathcal{C}}_{B'}, \operatorname{\mathcal{D}}) \simeq \operatorname{Fun}( (\Delta ^1 \times \operatorname{\mathcal{C}}_{B'}) / \operatorname{\mathcal{B}}, \operatorname{\mathcal{D}}) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{C}}/ \operatorname{\mathcal{B}}, \operatorname{\mathcal{D}}). \]
Unwinding the definitions, we see that $H|_{ \{ 0\} \times \operatorname{Fun}( \operatorname{\mathcal{C}}_{B'}, \operatorname{\mathcal{D}}) }$ is the functor given by precomposition with $f_{!}$, and that $H|_{ \{ 1\} \times \operatorname{Fun}( \operatorname{\mathcal{C}}_{B'}, \operatorname{\mathcal{D}}) }$ is the identity functor from $\operatorname{Fun}( \operatorname{\mathcal{C}}_{B'}, \operatorname{\mathcal{D}})$ to itself. It will therefore suffice to show that, for each object $F \in \operatorname{Fun}( \operatorname{\mathcal{C}}_{B'}, \operatorname{\mathcal{D}})$, the restriction $H|_{ \Delta ^1 \times \{ F\} }$ is a $\pi $-cartesian morphism of the $\infty $-category $\operatorname{Fun}( \operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{D}})$. By virtue of Corollary 5.3.6.8, this is equivalent to the assertion that the composite functor $\operatorname{\mathcal{C}}\xrightarrow {R} \operatorname{\mathcal{C}}_{B'} \xrightarrow {F} \operatorname{\mathcal{D}}$ carries $U$-cocartesian morphisms of $\operatorname{\mathcal{C}}$ to isomorphisms in $\operatorname{\mathcal{D}}$. This follows from our assumption on $R$, since the functor $F$ carries isomorphisms of $\operatorname{\mathcal{C}}_{B'}$ to isomorphisms of $\operatorname{\mathcal{D}}$.
$\square$