# Kerodon

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

Remark 5.1.0.1. Let $\mathrm{h} \mathit{\operatorname{Kan}}$ denote the homotopy category of Kan complexes (Construction 3.1.4.10). Then $\mathrm{h} \mathit{\operatorname{Kan}}$ can be identified with the homotopy category of the $\infty$-category $\operatorname{\mathcal{S}}$ of Construction 3.1.4.12. If $q: X \rightarrow S$ is a left fibration of simplicial sets, then Construction 5.1.1.7 determines a covariant transport functor

$T: \mathrm{h} \mathit{S} \rightarrow \mathrm{h} \mathit{\operatorname{Kan}}.$

In §, we show that (up to equivalence) $T$ can be promoted to a map of simplicial sets $S \rightarrow \operatorname{\mathcal{S}}$. In other words, the formation of covariant transport morphisms $(e: s \rightarrow s') \mapsto (e_{!}: X_{s} \rightarrow X_{s'})$ is compatible with composition not only up to homotopy, but up to coherent homotopy.