# Kerodon

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

Definition 5.1.1.1. Let $q: X \rightarrow S$ be a left fibration of simplicial sets, let $e: s \rightarrow s'$ be an edge of the simplicial set $S$, and let $f: X_{s} \rightarrow X_{s'}$ be a morphism of simplicial sets. We will say that $f$ is given by covariant transport along $e$ if there exists a commutative diagram of simplicial sets

$\xymatrix@R =50pt@C=50pt{ \Delta ^1 \times X_{s} \ar [r]^-{h} \ar [d] & X \ar [d]^{q} \\ \Delta ^{1} \ar [r]^-{e} & S }$

satisfying $h|_{ \{ 0\} \times X_{s} } = \operatorname{id}_{ X_ s }$, $h|_{ \{ 1\} \times X_{s} } = f$, and the left vertical map is given by projection onto the first factor. In this case, we also say that the morphism $h$ witnesses $f$ as given by covariant transport along $e$.