# Kerodon

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

Proposition 5.1.1.10. Let $q: X \rightarrow S$ be a left fibration of simplicial sets and let $e: s \rightarrow s'$ be an edge of of the simplicial set $S$. Then:

$(1)$

There exists a morphism of Kan complexes $g: X_{s'} \rightarrow X_{s}$ which is given by covariant transport along $e$.

$(2)$

Let $f: X_{s'} \rightarrow X_{s}$ be any morphism of Kan complexes. Then $f$ is given by covariant transport along $e$ if and only if it is homotopic to $g$.

Proof. Apply Proposition 5.1.1.4 to the opposite map $q^{\operatorname{op}}: X^{\operatorname{op}} \rightarrow S^{\operatorname{op}}$. $\square$