Kerodon

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

Proposition 5.2.5.1 (Transitivity). Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of simplicial sets and let $\sigma $ be a $2$-simplex of $\operatorname{\mathcal{C}}$, which we display as a diagram

\[ \xymatrix@R =50pt@C=50pt{ & D \ar [dr]^{g} & \\ C \ar [ur]^{f} \ar [rr]^-{h} & & E. } \]

Let $f_!: \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{D}$ and $g_!: \operatorname{\mathcal{E}}_{D} \rightarrow \operatorname{\mathcal{E}}_{E}$ be functors which are given by covariant transport along $f$ and $g$, respectively. Then the composite functor $(g_{!} \circ f_{!}): \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{E}$ is given by covariant transport along $h$.

Proof. Without loss of generality, we may replace $U$ by the projection map $\Delta ^{2} \times _{ \operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\rightarrow \Delta ^2$, and thereby reduce to the case where $\operatorname{\mathcal{C}}= \Delta ^2$ and $\sigma $ is the unique nondegenerate $2$-simplex of $\operatorname{\mathcal{C}}$. In this case, $\operatorname{\mathcal{E}}$ is an $\infty $-category. Let $u: \operatorname{id}_{ \operatorname{\mathcal{E}}_{C} } \rightarrow f_{!}$ be a morphism in the $\infty $-category $\operatorname{Fun}( \operatorname{\mathcal{E}}_{C}, \operatorname{\mathcal{E}})$ which witnesses $f_{!}$ as given by covariant transport along $f$, and let $v: \operatorname{id}_{ \operatorname{\mathcal{E}}_{D} } \rightarrow g_{!}$ be a morphism in the $\infty $-category $\operatorname{Fun}( \operatorname{\mathcal{E}}_{D}, \operatorname{\mathcal{E}})$ which witnesses $g_{!}$ as given by covariant transport along $g$. Let $v': f_{!} \rightarrow g_{!} \circ f_{!}$ denote the image of $v$ under the functor $\operatorname{Fun}( \operatorname{\mathcal{E}}_{D}, \operatorname{\mathcal{E}}) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{E}}_{C}, \operatorname{\mathcal{E}})$ given by precomposition with $f_!$. Let $w: \operatorname{id}_{\operatorname{\mathcal{E}}_{C}} \rightarrow g_{!} \circ f_{!}$ be a composition of $u$ with $v'$ in the $\infty $-category $\operatorname{Fun}( \operatorname{\mathcal{E}}_{C}, \operatorname{\mathcal{E}})$. We will complete the proof by showing that $w$ witnesses $g_{!} \circ f_{!}$ as given by covariant transport along $h$. To prove this, we must show that for every object $X \in \operatorname{\mathcal{E}}_{C}$, the the image $w_{X}: X \rightarrow ( g_{!} \circ f_{!})(X)$ is $U$-cocartesian. This follows from Corollary 5.1.2.4, since $w_{X}$ is a composition of the $U$-cocartesian morphisms $u_{X}: X \rightarrow f_{!}(X)$ and $v_{ f_{!}(X)}: f_{!}(X) \rightarrow (g_{!} \circ f_{!})(X)$. $\square$