Proposition 5.3.7.6. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category and let $f: X \rightarrow Y$ be a morphism of $\operatorname{\mathcal{C}}$. Then the diagram of $\infty $-categories
5.35
\begin{equation} \begin{gathered}\label{equation:covariant-transport-path-fibrations} \xymatrix { \operatorname{\mathcal{C}}_{/X} \ar [r]^{ f \circ } \ar [d]^{ \delta _{/X} }_{\sim } & \operatorname{\mathcal{C}}_{/Y} \ar [d]^{\delta _{/Y} }_{\sim } \\ \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{ \operatorname{\mathcal{C}}} \{ X\} \ar [r]^{ f_{!} } & \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \{ Y \} } \end{gathered} \end{equation}
commutes up to isomorphism. Here the vertical maps are the pinch inclusion equivalences of Corollary 4.6.4.18, the upper horizontal map is the composition functor of Example 4.3.6.15, and the lower horizontal map is given by covariant transport for the evaluation functor $U: \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{C}}$.
Proof.
Consider the restriction maps
\[ \operatorname{\mathcal{C}}_{/X} \xleftarrow {e_0} \operatorname{\mathcal{C}}_{/f} \xrightarrow {e_1} \operatorname{\mathcal{C}}_{/Y}. \]
Since the inclusion map $\{ 0\} \hookrightarrow \Delta ^1$ is left anodyne, $e_0$ is a trivial Kan fibration (Corollary 4.3.6.14). By construction, the composition functor of Example 4.3.6.15 is given by the composition $(e_{1} \circ e_0^{-1}): \operatorname{\mathcal{C}}_{/X} \rightarrow \operatorname{\mathcal{C}}_{/Y}$, where $e_0^{-1}$ is a homotopy inverse to $e_0$. The covariant transport functor $f_{!}$ admits a similar description. Let $\operatorname{\mathcal{E}}$ denote the oriented fiber product $\operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}}) \operatorname{\vec{\times }}_{ \operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{C}}) } \{ f \} $, whose objects are given by commutative diagrams
\[ \xymatrix { X' \ar [r]^{f'} \ar [d] & Y' \ar [d] \\ X \ar [r] & Y } \]
in the $\infty $-category $\operatorname{\mathcal{C}}$, and let $\operatorname{\mathcal{E}}^{0}$ denote the full subcategory of $\operatorname{\mathcal{E}}$ spanned by those diagrams where $f'$ is an isomorphism. Evaluation at the vertices $0,1 \in \Delta ^1$ then determines forgetful functors $e'_0: \operatorname{\mathcal{E}}^{0} \rightarrow \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{ \operatorname{\mathcal{C}}} \{ X\} $ and $e'_1: \operatorname{\mathcal{E}}^{0} \rightarrow \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \{ Y\} $. It follows from Proposition 5.3.7.2 that we can identify $\operatorname{\mathcal{E}}^{0}$ with the $\infty $-category of $U$-cocartesian lifts of the morphism $f$. It follows that $e'_0$ is a trivial Kan fibration, and that the functor $f_{!}$ is given by the composition
\[ (e'_0 \circ e'^{-1}_{0}): \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \{ X\} \rightarrow \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \{ Y\} , \]
where $e'^{-1}_{0}$ is a homotopy inverse of $e'_0$. Consequently, to show that the diagram (5.35) commutes up to isomorphism, it will suffice to show that there is a commutative diagram of simplicial sets
\[ \xymatrix { \operatorname{\mathcal{C}}_{/X} \ar [d]^{ \delta _{/X} }_{\sim } & \operatorname{\mathcal{C}}_{/f} \ar [d] \ar [l]_{e_0} \ar [r]^{ e_1} & \operatorname{\mathcal{C}}_{/Y} \ar [d]^{\delta _{/Y} }_{\sim } \\ \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{ \operatorname{\mathcal{C}}} \{ X\} & \operatorname{\mathcal{E}}^{0} \ar [l]_{ e'_0 } \ar [r]^{ e'_1 } & \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \{ Y \} . } \]
For $v \in \{ 0,1\} $, let $\underline{v}: \operatorname{\mathcal{C}}_{/f} \rightarrow \Delta ^1$ denote the constant functor taking the value $v$. We then have a commutative diagram
\[ \xymatrix { \operatorname{id}_{ \operatorname{\mathcal{C}}_{/f} } \ar [r]^{\operatorname{id}} \ar [d] & \operatorname{id}_{ \operatorname{\mathcal{C}}_{/f} } \\ \underline{0}_{ \operatorname{\mathcal{C}}_{/f} } & \underline{1}_{ \operatorname{\mathcal{C}}_{/f} } } \]
in the $\infty $-category of functors from $\operatorname{\mathcal{C}}_{/f}$ to the join $\operatorname{\mathcal{C}}_{/f} \star \Delta ^1$. Postcomposing with the tautological map $\operatorname{\mathcal{C}}_{/f} \star \Delta ^1 \rightarrow \operatorname{\mathcal{C}}$, we obtain a functor
\[ T: \operatorname{\mathcal{C}}_{/f} \rightarrow \operatorname{\mathcal{E}}^{0} \subseteq \operatorname{Fun}( \Delta ^1 \times \Delta ^1, \operatorname{\mathcal{C}}) \]
with the desired properties.
$\square$