Remark 5.2.2.14 (05J5): Functoriality

Remark 5.2.2.14 (Functoriality). Suppose we are given a commutative diagram of simplicial sets

\[ \xymatrix { \operatorname{\mathcal{E}}\ar [rr]^{T} \ar [dr]^{U} & & \operatorname{\mathcal{E}}' \ar [dl]_{U'} \\ & \operatorname{\mathcal{C}}, & } \]

where $U$ and $U'$ are cocartesian fibrations and $T$ carries $U$-cocartesian edges of $\operatorname{\mathcal{E}}$ to $U'$-cocartesian edges of $\operatorname{\mathcal{E}}'$. Let $f: C \rightarrow D$ be an edge of $\cal $, and let $F: \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{D}$ and $F': \operatorname{\mathcal{E}}'_{C} \rightarrow \operatorname{\mathcal{E}}'_{D}$ be a given by covariant transport along $f$. Then the diagram of $\infty $-categories

\[ \xymatrix { \operatorname{\mathcal{E}}_{C} \ar [r]^{ F } \ar [d]^{ T_ C } & \operatorname{\mathcal{E}}_{D} \ar [d]^{ T_ D } \\ \operatorname{\mathcal{E}}'_{C} \ar [r]^{F'} & \operatorname{\mathcal{E}}'_{D} } \]

commutes up to isomorphism. To prove this, choose diagrams $\widetilde{F}: \Delta ^1 \times \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}$ and $\widetilde{F}': \Delta ^1 \times \operatorname{\mathcal{E}}'_{C} \rightarrow \operatorname{\mathcal{E}}'$ which exhibit $F$ and $F'$ as given by covariant transport along $F$. Then the morphisms

\[ T \circ \widetilde{F}, \widetilde{F}' \circ ( \operatorname{id}_{\Delta ^1} \times T_{C} ): \Delta ^1 \times \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}' \]

are $U'$-cocartesian lifts of the map $\Delta ^1 \times \operatorname{\mathcal{E}}_{C} \rightarrow \Delta ^1 \xrightarrow {f} \operatorname{\mathcal{C}}$ which coincide when restricted to $\{ 0\} \times \operatorname{\mathcal{E}}_{C}$, and are therefore isomorphic when restricted to $\{ 1\} \times \operatorname{\mathcal{E}}_{C}$ (Lemma 5.2.2.13).