Kerodon

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

Remark 5.6.1.18 (Covariant Transport). Let $\operatorname{\mathcal{C}}$ be a category, let $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \mathbf{Cat}$ be a functor of $2$-categories, and let $U: \int _{\operatorname{\mathcal{C}}} \mathscr {F} \rightarrow \operatorname{\mathcal{C}}$ be the forgetful functor of Notation 5.6.1.11. For each object $C \in \operatorname{\mathcal{C}}$, let

\[ \iota _{C}: \mathscr {F}(C) \simeq \{ C \} \times _{\operatorname{\mathcal{C}}} \int _{\operatorname{\mathcal{C}}} \mathscr {F} \subseteq \int _{\operatorname{\mathcal{C}}} \mathscr {F} \]

be the isomorphism of Remark 5.6.1.12. Note that every morphism $f: C \rightarrow D$ in $\operatorname{\mathcal{C}}$ determines a natural transformation of functors $\widetilde{f}: \iota _{C} \rightarrow \iota _{D} \circ \mathscr {F}(f)$, which carries an object $X \in \mathscr {F}(C)$ to the $U$-cocartesian morphism $(f, \operatorname{id}): (C,X) \rightarrow (D, \mathscr {F}(f)(X) )$. It follows that $\widetilde{f}$ identifies $\mathscr {F}(f)$ with the covariant transport functor $f_{!}$ of Notation 5.2.2.2.