# Kerodon

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

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}}'. }$