Kerodon

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

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

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}\ar [d]^-{U} \ar [r]^-{G} & \operatorname{\mathcal{E}}' \ar [d]^-{U'} \\ \operatorname{\mathcal{C}}\ar [r]^-{\overline{G}} & \operatorname{\mathcal{C}}', } \]

where $U$ and $U'$ are cocartesian fibrations. Let $C$ and $D$ be vertices of $\operatorname{\mathcal{C}}$ having images $C' = \overline{G}(C)$ and $D' = \overline{G}(D)$, respectively, so that $G$ induces functors $G_{C}: \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}'_{C'}$ and $G_{D}: \operatorname{\mathcal{E}}_{D} \rightarrow \operatorname{\mathcal{E}}'_{D'}$. Let $\varphi : \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D) \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{C}}'}(C',D')$ be the morphism induced by $\overline{G}$, and let

\[ F: \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D) \times \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{D} \quad \quad F': \operatorname{Hom}_{\operatorname{\mathcal{C}}'}(C',D') \times \operatorname{\mathcal{E}}'_{C'} \rightarrow \operatorname{\mathcal{E}}'_{D'} \]

be given by parametrized covariant transport with respect to $U$ and $U'$. Suppose that the morphism $G$ carries $U$-cocartesian edges of $\operatorname{\mathcal{E}}$ to $U'$-cocartesian edges of $\operatorname{\mathcal{E}}'$. Then the diagram

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D) \times \operatorname{\mathcal{E}}_{C} \ar [r]^-{F} \ar [d]^{ \varphi \times G_{C} } & \operatorname{\mathcal{E}}_{D} \ar [d]^{G_ D} \\ \operatorname{Hom}_{\operatorname{\mathcal{C}}'}(C',D') \times \operatorname{\mathcal{E}}'_{C'} \ar [r]^-{F'} & \operatorname{\mathcal{E}}'_{D'} } \]

commutes up to isomorphism: that is, $G_{D} \circ F$ and $F' \circ (\varphi \times G_{C})$ are isomorphic as objects of the $\infty $-category $\operatorname{Fun}( \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D) \times \operatorname{\mathcal{E}}_{C}, \operatorname{\mathcal{E}}'_{D'} )$. This follows by applying the uniqueness assertion of Lemma 5.2.2.9 to the lifting problem

\[ \xymatrix@R =50pt@C=50pt{ \{ 0\} \times \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D) \times \operatorname{\mathcal{E}}_{C} \ar [r] \ar [d] & \operatorname{\mathcal{E}}' \ar [d]^{U'} \\ \Delta ^1 \times \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D) \times \operatorname{\mathcal{E}}_{C} \ar [r] \ar@ {-->}[ur] & \operatorname{\mathcal{C}}'. } \]