Kerodon

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 morphism $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$