$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Corollary 5.3.1.9 (Functoriality). Suppose we are given a commutative diagram of $\infty $-categories
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}\ar [dr]^{U} \ar [rr]^{F} & & \operatorname{\mathcal{E}}' \ar [dl]_{U'} \\ & \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}), & } \]
where $U$ and $U'$ are cocartesian fibrations. The following conditions are equivalent:
- $(1)$
The functor $F$ carries $U$-cocartesian morphisms of $\operatorname{\mathcal{E}}$ to $U'$-cocartesian morphisms of $\operatorname{\mathcal{E}}'$.
- $(2)$
The induced map of weak transport representations $\operatorname{wTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}} \rightarrow \operatorname{wTr}_{\operatorname{\mathcal{E}}'/\operatorname{\mathcal{C}}}$ carries $\operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$ into $\operatorname{sTr}_{\operatorname{\mathcal{E}}'/\operatorname{\mathcal{C}}}$.
Proof.
The implication $(1) \Rightarrow (2)$ is immediate from the definitions. Conversely, suppose that condition $(2)$ is satisfied, and let $f: X \rightarrow Y$ be a $U$-cocartesian morphism of $\operatorname{\mathcal{E}}$; we wish to show that $F(f)$ is $U'$-cocartesian. Set $C = U(X)$. Using Proposition 5.3.1.7, we can choose an object $\widetilde{X} \in \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(C)$ satisfying $\operatorname{ev}_{C}(\widetilde{X}) = X$. Let us identify $\widetilde{X}$ with a functor of $\infty $-categories $G: \operatorname{N}_{\bullet }( \operatorname{\mathcal{C}}_{C/} ) \rightarrow \operatorname{\mathcal{E}}$. Write $\overline{f}$ for the image $U(f)$, which we regard as a morphism in the coslice category $\operatorname{\mathcal{C}}_{C/}$. Assumption $(2)$ guarantees that $F$ carries $\widetilde{X}$ to an object of $\operatorname{sTr}_{\operatorname{\mathcal{E}}'/\operatorname{\mathcal{C}}}(C)$, so that $(F \circ G)(\overline{f} )$ is a $U'$-cocartesian morphism of $\operatorname{\mathcal{E}}'$. Since $f$ is isomorphic to $G( \overline{f} )$ (as an object of the $\infty $-category $\operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{E}})$), it follows that $F(f)$ is also $U'$-cocartesian.
$\square$