Kerodon

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

Proposition 5.1.1.6 (Transitivity). Let $q: X \rightarrow S$ be a left fibration of simplicial sets and let $\sigma $ be a $2$-simplex of $S$, whose faces we display as a diagram

\[ \xymatrix@R =50pt@C=50pt{ & s' \ar [dr]^{e'} & \\ s \ar [ur]^{e} \ar [rr]^{e''} & & s''. } \]

Let $f: X_{s} \rightarrow X_{s'}$ be a morphism of Kan complexes given by covariant transport along $e$, and let $f': X_{s'} \rightarrow X_{s''}$ be a morphism of Kan complexes given by covariant transport along $e'$. Then the composite map $(f' \circ f): X_{s} \rightarrow X_{s''}$ is given by covariant transport along $e''$.

Proof. For every simplex $\tau $ of the simplicial set $S$, let $\underline{\tau }$ denote its image in the simplicial set $\operatorname{Fun}(X_ s, S)$. Let $Q: \operatorname{Fun}( X_ s, X) \rightarrow \operatorname{Fun}( X_ s, S)$ be given by postcomposition with $q$. Note that the inclusion map $X_{s} \hookrightarrow X$, the morphism $f: X_{s} \rightarrow X_{s'}$, and the composite map $(f' \circ f): X_{s} \rightarrow X_{s''}$ can be identified with vertices $\overline{s}$, $\overline{s}'$, and $\overline{s}''$ of the simplicial set $\operatorname{Fun}( X_ s, X)$ satisfying $Q( \overline{s} ) = \underline{s}$, $Q( \overline{s}' ) = \underline{s}'$, and $Q( \overline{s}'') = \underline{s}''$. Let $h: \Delta ^1 \times X_{s} \rightarrow X$ witness $f$ as given by covariant transport along $e$, and let $h': \Delta ^1 \times X_{s'} \rightarrow X$ witness $f'$ as given by covariant transport along $e'$. Then $h$ can be identified with an edge $\overline{e}: \overline{s} \rightarrow \overline{s}'$ of the simplicial set $\operatorname{Fun}( X_ s, X)$ satisfying $Q( \overline{e} ) = \underline{e}$. Similarly, the composite map

\[ \Delta ^1 \times X_ s \xrightarrow { \operatorname{id}\times f} \Delta ^1 \times X_{s'} \xrightarrow {h'} X \]

can be identified with an edge $\overline{e}'$ of $\operatorname{Fun}(X_ s, X)$ satisfying $Q( \overline{e}' ) = \underline{e}'$. Since $Q$ is a left fibration (Corollary 4.2.3.2), the lifting problem

\[ \xymatrix@R =50pt@C=50pt{ \Lambda ^{2}_{1} \ar [r]^-{ ( \overline{e}', \bullet , \overline{e} ) } \ar [d] & \operatorname{Fun}( X_ s, X) \ar [d]^{Q} \\ \Delta ^2 \ar [r]^-{ \underline{\sigma } } \ar@ {-->}[ur]^{ \overline{\sigma } } & \operatorname{Fun}(X_ s, S) } \]

admits a solution. Unwinding the definitions, we see that $d_1( \overline{\sigma } )$ can be identified with a map of simplicial sets $\Delta ^1 \times X_{s} \rightarrow X$ which witnesses $f' \circ f$ as given by covariant transport along $e''$. $\square$