Proposition 5.2.8.8. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of $\infty $-categories. Let $C$, $D$, and $E$ be objects of $\operatorname{\mathcal{C}}$, and let
\[ F: \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D) \times \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{D} \quad \quad G: \operatorname{Hom}_{\operatorname{\mathcal{C}}}(D,E) \times \operatorname{\mathcal{E}}_{D} \rightarrow \operatorname{\mathcal{E}}_{E} \]
\[ H: \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,E) \times \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{E} \]
be given by parametrized covariant transport. Then the diagram
5.25
\begin{equation} \begin{gathered}\label{equation:transitivity-parametrized} \xymatrix@R =50pt@C=50pt{ \operatorname{Hom}_{\operatorname{\mathcal{C}}}(D,E) \times \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D) \times \operatorname{\mathcal{E}}_{C} \ar [r]^-{ \operatorname{id}\times F } \ar [d] & \operatorname{Hom}_{\operatorname{\mathcal{C}}}(D,E) \times \operatorname{\mathcal{E}}_{D} \ar [d]^{ G } \\ \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,E) \times \operatorname{\mathcal{E}}_{C} \ar [r]^-{ H } & \operatorname{\mathcal{E}}_{E} } \end{gathered} \end{equation}
commutes in the homotopy category $\mathrm{h} \mathit{\operatorname{QCat}}$; here the left vertical map is given by the composition law of Construction 4.6.9.9.
Proof.
Let $\operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D,E)$ be the Kan complex defined in Notation 4.6.9.1, let $H'$ denote the composite map
\[ \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D,E) \times \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,E) \times \operatorname{\mathcal{E}}_{C} \xrightarrow {H} \operatorname{\mathcal{E}}_{E}, \]
and let $H''$ denote the composition
\begin{eqnarray*} \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D,E) \times \operatorname{\mathcal{E}}_{C} & \rightarrow & \operatorname{Hom}_{\operatorname{\mathcal{C}}}(D,E) \times \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D) \times \operatorname{\mathcal{E}}_{C} \\ & \xrightarrow {F} & \operatorname{Hom}_{\operatorname{\mathcal{C}}}(D,E) \times \operatorname{\mathcal{E}}_{D} \\ & \xrightarrow {G} & \operatorname{\mathcal{E}}_{E}. \end{eqnarray*}
We will show that $H'$ and $H''$ are isomorphic when regarded as objects of the $\infty $-category $\operatorname{Fun}( \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D,E) \times \operatorname{\mathcal{E}}_{C}, \operatorname{\mathcal{E}}_{E} )$. The homotopy commutativity of the diagram (5.25) will then follow by precomposing with any section of the trivial Kan fibration $\operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D,E) \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{C}}}(D,E) \times \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D)$.
Choose morphisms
\[ \widetilde{F}: \operatorname{N}_{\bullet }( \{ 0 < 1 \} ) \times \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D) \times \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}} \]
\[ \widetilde{G}: \operatorname{N}_{\bullet }( \{ 1 < 2 \} ) \times \operatorname{Hom}_{\operatorname{\mathcal{C}}}(D,E) \times \operatorname{\mathcal{E}}_{D} \rightarrow \operatorname{\mathcal{E}} \]
\[ \widetilde{H}: \operatorname{N}_{\bullet }( \{ 0 < 2 \} ) \times \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,E) \times \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}} \]
which witness $F$, $G$, and $H$ as given by parametrized covariant transport, respectively. Composing with the projection maps
\[ \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D) \leftarrow \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D,E) \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,E), \]
we obtain morphisms
\[ \widetilde{F}': \operatorname{N}_{\bullet }( \{ 0 < 1 \} ) \times \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D,E) \times \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}} \]
\[ \widetilde{H}': \operatorname{N}_{\bullet }( \{ 0 < 2 \} ) \times \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D,E) \times \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}. \]
Let $\widetilde{G}'$ denote the composite map
\begin{eqnarray*} \operatorname{N}_{\bullet }( \{ 1 < 2\} ) \times \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D,E) \times \operatorname{\mathcal{E}}_{C} \hspace{-.5em} & \rightarrow & \operatorname{N}_{\bullet }( \{ 1 < 2\} ) \times \operatorname{Hom}_{\operatorname{\mathcal{C}}}(D,E) \times \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D) \times \operatorname{\mathcal{E}}_{C} \\ & \xrightarrow { F } & \operatorname{N}_{\bullet }( \{ 1 < 2 \} ) \times \operatorname{Hom}_{\operatorname{\mathcal{C}}}(D,E) \times \operatorname{\mathcal{E}}_{D} \\ & \xrightarrow { \widetilde{G} } & \operatorname{\mathcal{E}}. \end{eqnarray*}
Since $U$ is an inner fibration, the lifting problem
\[ \xymatrix@C =100pt@R=50pt{ \Lambda ^{2}_{1} \times \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D,E) \times \operatorname{\mathcal{E}}_{C} \ar [r]^-{ ( \widetilde{G}', \bullet , \widetilde{F}' ) } \ar [d] & \operatorname{\mathcal{E}}\ar [d]^{U} \\ \Delta ^2 \times \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D,E) \times \operatorname{\mathcal{E}}_{C} \ar [r] \ar@ {-->}[ur]^{\Phi } & \operatorname{\mathcal{C}}} \]
admits a solution $\Phi : \Delta ^2 \times \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D,E) \times \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}$. Let $\widetilde{H}''$ denote the restriction of $\Phi $ to the product $\operatorname{N}_{\bullet }( \{ 0, 2\} ) \times \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D,E) \times \operatorname{\mathcal{E}}_{C}$. Using Proposition 5.1.4.13, we see that $\widetilde{H}''$ is a $U$-cocartesian lift of $U \circ \widetilde{H}'' = U \circ \widetilde{H}'$, in the sense of Definition 5.2.2.10. Applying the uniqueness assertion of Lemma 5.2.2.13, we conclude that the restrictions $H' = \widetilde{H}'|_{ \{ 2\} \times \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D,E) \times \operatorname{\mathcal{E}}_{C} }$ and $H'' = \widetilde{H}''|_{ \{ 2\} \times \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D,E) \times \operatorname{\mathcal{E}}_{C} }$ are isomorphic when regarded as objects of the $\infty $-category $\operatorname{Fun}( \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D,E) \times \operatorname{\mathcal{E}}_{C}, \operatorname{\mathcal{E}}_{E})$, as desired.
$\square$