# Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$ $\newcommand\empty{}$

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{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}$$

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.8.9.

Proof. Let $\operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D,E)$ be the Kan complex defined in Notation 4.6.8.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.12, 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$