Kerodon

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

Remark 5.1.1.3. Suppose we are given a pullback diagram of simplicial sets

\[ \xymatrix@R =50pt@C=50pt{ \overline{X} \ar [d]^{ \overline{q} } \ar [r] & X \ar [d]^{q} \\ \overline{S} \ar [r] & S. } \]

Let $\overline{e}: \overline{s} \rightarrow \overline{s}'$ be an edge of the simplicial set $\overline{S}$ having image $e: s \rightarrow s'$ in the simplicial set $S$. Then a morphism of Kan complexes $f: \overline{X}_{ \overline{s} } \rightarrow \overline{X}_{ \overline{s}' }$ is given by covariant transport along $\overline{e}$ if and only if, when viewed as a morphism from $X_{s}$ to $X_{s'}$, it is given by covariant transport along $e$.