# Kerodon

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

Proposition 5.2.8.7. Let $\operatorname{\mathcal{C}}$ be an $\infty$-category containing objects $C$, $D$, and $E$. Then the composition law

$\circ : \operatorname{Hom}_{\operatorname{\mathcal{C}}}(D,E) \times \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D) \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,E)$

of Construction 4.6.8.9 is given by parametrized covariant transport for the left fibration $U: \{ C\} \operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}$ (in the sense of Definition 5.2.8.1), and also by parametrized contravariant transport for the right fibration $V: \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \{ E\} \rightarrow \operatorname{\mathcal{C}}$.

Proof. We will prove the first assertion; the second follows by a similar argument. Let $S: \Delta ^1 \times \Delta ^1 \rightarrow \Delta ^2$ be the morphism given on vertices by the formula $T(i,j) = i(j+1)$, and let $T$ be a 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)$ (see Corollary 4.6.8.5). Then the composite map

$\Delta ^1 \times \Delta ^1 \times \operatorname{Hom}_{\operatorname{\mathcal{C}}}(D,E) \times \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D) \xrightarrow {S \times T} \Delta ^2 \times \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D,E) \rightarrow \operatorname{\mathcal{C}}$

carries $\{ 0\} \times \Delta ^1 \times \operatorname{Hom}_{\operatorname{\mathcal{C}}}(D,E) \times \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D)$ to the vertex $C$, and can therefore be identified with a functor

$\widetilde{F}: \Delta ^1 \times \operatorname{Hom}_{\operatorname{\mathcal{C}}}(D,E) \times \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D) \rightarrow \{ C\} \operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}.$

which exhibits the composition law as given by parametrized covariant transport for the left fibration $U$. $\square$