Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$

Definition 5.1.1.8. Let $q: X \rightarrow S$ be a right fibration of simplicial sets, let $e: s \rightarrow s'$ be an edge of the simplicial set $S$, and let $g: X_{s'} \rightarrow X_{s}$ be a morphism of simplicial sets. We will say that $g$ is given by contravariant 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|_{ \{ 1\} \times X_{s'} } = \operatorname{id}_{ X_{s'} }$, $h|_{ \{ 0\} \times X_{s} } = g$, and the left vertical map is given by projection onto the first factor.