Kerodon

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

5.5.2 Elements of Category-Valued Functors

We now generalize Construction 5.5.1.1 and Variant 5.5.1.2 to the setting of category-valued functors. Throughout this section, we let $\mathbf{Cat}$ denote the (strict) $2$-category of small categories (Example 2.2.0.4).

Definition 5.5.2.1 (The Category of Elements: Covariant Version). Let $\operatorname{\mathcal{C}}$ be a category and let $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \mathbf{Cat}$ be a functor of $2$-categories. We define a category $\int _{\operatorname{\mathcal{C}}} \mathscr {F}$ as follows:

  • The objects of $\int _{\operatorname{\mathcal{C}}} \mathscr {F}$ are pairs $(C, X)$, where $C$ is an object of $\operatorname{\mathcal{C}}$ and $X$ is an object of the category $\mathscr {F}(C)$.

  • Let $(C,X)$ and $(D,Y)$ be objects of $\int _{\operatorname{\mathcal{C}}} \mathscr {F}$. Then a morphism from $(C,X)$ to $(D,Y)$ in the category $\int _{\operatorname{\mathcal{C}}} \mathscr {F}$ is a pair $(f,u)$, where $f: C \rightarrow D$ is a morphism in the category $\operatorname{\mathcal{C}}$ and $u: \mathscr {F}(f)(X) \rightarrow Y$ is a morphism in the category $\mathscr {F}(D)$.

  • Let $(f,u): (C,X) \rightarrow (D,Y)$ and $(g,v): (D,Y) \rightarrow (E,Z)$ be morphisms in the category $\int _{\operatorname{\mathcal{C}}} \mathscr {F}$. Then the composition $(g,v) \circ (f,u)$ is the pair $(g \circ f, w)$, where $w: \mathscr {F}(g \circ f)(X) \rightarrow Z$ is the morphism of $\mathscr {F}(E)$ given by the composition

    \[ \mathscr {F}(g \circ f)(X) \xrightarrow { \mu _{g,f}^{-1}(X) } (\mathscr {F}(g) \circ \mathscr {F}(f))(X) \xrightarrow { \mathscr {F}(g)(u) } \mathscr {F}(g)(Y) \xrightarrow {v} Z, \]

    where $\mu _{g,f}: \mathscr {F}(g) \circ \mathscr {F}(f) \simeq \mathscr {F}(g \circ f)$ denotes the composition constraint for the functor $\mathscr {F}$.

We will refer to $\int _{\operatorname{\mathcal{C}}} \mathscr {F}$ as the category of elements of $\mathscr {F}$.

Proposition 5.5.2.2. Let $\operatorname{\mathcal{C}}$ be a category and let $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \mathbf{Cat}$ be a functor of $2$-categories. Then the category of elements $\int _{\operatorname{\mathcal{C}}} \mathscr {F}$ is well-defined: that is, the composition law described in Definition 5.5.2.1 is unital and associative.

Proof. Let $(D,Y)$ be an object of $\int _{\operatorname{\mathcal{C}}} \mathscr {F}$. We let $\operatorname{id}_{ (D,Y)}$ denote the morphism from $(D,Y)$ to itself given by the pair $(\operatorname{id}_{D}, \epsilon _{D}^{-1}(Y) )$, where $\epsilon _{D}: \mathscr {F}( \operatorname{id}_{D} ) \simeq \operatorname{id}_{ \mathscr {F}(D) }$ is the identity constraint for the functor $\mathscr {F}$. We first show that $\operatorname{id}_{(D,Y)}$ is a (two-sided) unit for the composition law on $\int _{\operatorname{\mathcal{C}}} \mathscr {F}$. We consider two cases:

  • Let $(C,X)$ be another object of $\int _{\operatorname{\mathcal{C}}} \mathscr {F}$ and let $(f,u): (C,X) \rightarrow (D,Y)$ be a morphism in $\int _{\operatorname{\mathcal{C}}} \mathscr {F}$. We wish to show that the composition $\operatorname{id}_{(D,Y)} \circ (f,u)$ is equal to $(f,u)$ (as a morphism from $(C,X)$ to $(D,Y)$). Unwinding the definitions, this is equivalent to the assertion that the morphism $u: \mathscr {F}(f)(X) \rightarrow Y$ is equal to the composition

    \[ \mathscr {F}(f)(X) \xrightarrow { \mu _{\operatorname{id}_{D}, f}^{-1}(X) } (\mathscr {F}(\operatorname{id}_ D) \circ \mathscr {F}(f))(X) \xrightarrow { \mathscr {F}(\operatorname{id}_ D)(u)} \mathscr {F}(\operatorname{id}_{D})(Y) \xrightarrow { \epsilon _{D}^{-1}(Y) } Y. \]

    Using the commutativity of the diagram

    \[ \xymatrix@R =50pt@C=50pt{ (\mathscr {F}(\operatorname{id}_ D) \circ \mathscr {F}(f))(X) \ar [r]^-{ \epsilon _{D}(\mathscr {F}(f)(X)) }_-{\sim } \ar [d]^-{ \mathscr {F}(\operatorname{id}_ D)(u) } & \mathscr {F}(f)(X) \ar [d]^-{u} \\ \mathscr {F}(\operatorname{id}_ D)(Y) \ar [r]^-{ \epsilon _{D}(Y) }_-{\sim } & Y, } \]

    we are reduced to showing that the composition

    \[ \mathscr {F}(f)(X) \xrightarrow { \mu _{\operatorname{id}_{D}, f}^{-1}(X) } (\mathscr {F}(\operatorname{id}_ D) \circ \mathscr {F}(f))(X) \xrightarrow { \epsilon _{D}^{-1}( \mathscr {F}(f)(X) )} \mathscr {F}(f)(X) \]

    is equal to the identity, which follows from axiom $(a)$ of Definition 2.2.4.5.

  • Let $(E,Z)$ be another object of $\int _{\operatorname{\mathcal{C}}} \mathscr {F}$, and let $(g,v): (D,Y) \rightarrow (E,Z)$ be a morphism in $\int _{\operatorname{\mathcal{C}}} \mathscr {F}$. We wish to show that the composition $(g,v) \circ \operatorname{id}_{(D,Y)}$ is equal to $(g,v)$ (as a morphism from $(D,Y)$ to $(E,Z)$). Unwinding the definitions, this is equivalent to the assertion that the morphism $v: \mathscr {F}(g)(Z) \rightarrow Y$ is equal to the composition

    \[ \mathscr {F}(g)(Y) \xrightarrow { \mu _{g, \operatorname{id}_ D}^{-1}(Y) } (\mathscr {F}(g) \circ \mathscr {F}(\operatorname{id}_ D))(Y) \xrightarrow { \mathscr {F}(g)( \epsilon _{D}^{-1}(Y) )} \mathscr {F}(g)(Y) \xrightarrow { v} Z, \]

    which follows from from axiom $(b)$ of Definition 2.2.4.5.

We now show that composition of morphisms in $\int _{\operatorname{\mathcal{C}}} \mathscr {F}$ is associative. Suppose we are given a composable sequence

\[ (B,W) \xrightarrow { (e,t) } (C,X) \xrightarrow { (f,u) } (D,Y) \xrightarrow { (g,v) } (E,Z) \]

of morphisms of $\int _{\operatorname{\mathcal{C}}} \mathscr {F}$. Unwinding the definitions, we obtain equalities

\[ (g,v) \circ ( (f,u) \circ (e,t) ) = (g \circ f \circ e, v \circ \mathscr {F}(g)(u) \circ w) \]

\[ ( (g,v) \circ (f,u) ) \circ (e,t) ) = (g \circ f \circ e, v \circ \mathscr {F}(g)(u) \circ w') \]

where $w,w': \mathscr {F}(g \circ f \circ e)(W) \rightarrow (\mathscr {F}(e) \circ \mathscr {F}(f))(X)$ are the morphisms in the category $\mathscr {F}(E)$ given by clockwise and counterclockwise composition in the diagram

\[ \xymatrix@R =50pt@C=50pt{ \mathscr {F}(g \circ f \circ e)(W) \ar [r]^-{ \mu _{g, f \circ e}^{-1}(W) }_-{\sim } \ar [d]^-{ \mu _{g \circ f, e}^{-1}(W) }_-{\sim } & (\mathscr {F}(g) \circ \mathscr {F}(f \circ e))(W) \ar [d]^-{\mathscr {F}(g)( \mu _{f,e}^{-1}(W) )}_-{\sim } \\ (\mathscr {F}(g \circ f) \circ \mathscr {F}(e))(W) \ar [r]^-{ \mu _{g,f}^{-1}( \mathscr {F}(e)(W) )}_-{\sim } \ar [d]^{ \mathscr {F}(g \circ f)(t) } & (\mathscr {F}(g) \circ \mathscr {F}(f) \circ \mathscr {F}(e))(W) \ar [d]^-{ (\mathscr {F}(g) \circ \mathscr {F}(f))(t)} \\ \mathscr {F}(g \circ f)(X) \ar [r]^-{ \mu _{g,f}^{-1}(X) }_-{\sim } & (\mathscr {F}(g) \circ \mathscr {F}(f))(X).} \]

It will therefore suffice to show that this diagram commutes. For the upper square, this follows from axiom $(c)$ of Definition 2.2.4.5. For the lower square, it follows from the naturality of the composition constraint $\mu _{g,f}$. $\square$

Definition 5.5.2.1 has a counterpart for contravariant functors:

Definition 5.5.2.3 (The Category of Elements: Contravariant Version). Let $\operatorname{\mathcal{C}}$ be a category and let $\mathscr {F}: \operatorname{\mathcal{C}}^{\operatorname{op}} \rightarrow \mathbf{Cat}$ be a functor of $2$-categories (Definition 2.2.4.5). We define a category $\int ^{\operatorname{\mathcal{C}}} \mathscr {F}$ as follows:

  • The objects of $\int ^{\operatorname{\mathcal{C}}} \mathscr {F}$ are pairs $(C, X)$, where $C$ is an object of $\operatorname{\mathcal{C}}$ and $X$ is an object of the category $\mathscr {F}(C)$.

  • Let $(C,X)$ and $(D,Y)$ be objects of $\int ^{\operatorname{\mathcal{C}}} \mathscr {F}$. Then a morphism from $(C,X)$ to $(D,Y)$ in the category $\int ^{\operatorname{\mathcal{C}}} \mathscr {F}$ is a pair $(f,u)$, where $f: C \rightarrow D$ is a morphism in the category $\operatorname{\mathcal{C}}$ and $u: X \rightarrow \mathscr {F}(f)(Y)$ is a morphism in the category $\mathscr {F}(C)$.

  • Let $(f,u): (C,X) \rightarrow (D,Y)$ and $(g,v): (D,Y) \rightarrow (E,Z)$ be morphisms in the category $\int ^{\operatorname{\mathcal{C}}} \mathscr {F}$. Then the composition $(g,v) \circ (f,u)$ is the pair $(g \circ f, w)$, where $w: X \rightarrow \mathscr {F}( g \circ f)(Z)$ is the morphism of $\mathscr {F}(C)$ given by the composition

    \[ X \xrightarrow { u } \mathscr {F}(f)(Y) \xrightarrow { \mathscr {F}(f)(v) } (\mathscr {F}(f) \circ \mathscr {F}(g))(Z) \xrightarrow { \mu _{f,g}(Z) } \mathscr {F}(g \circ f)(Z), \]

    where $\mu _{f,g}: \mathscr {F}(f) \circ \mathscr {F}(g) \simeq \mathscr {F}( g \circ f)$ denotes the composition constraint for the lax functor $\mathscr {F}$.

We will refer to $\int ^{\operatorname{\mathcal{C}}} \mathscr {F}$ as the category of elements of the functor $\mathscr {F}$.

Remark 5.5.2.4. The category of elements $\int ^{\operatorname{\mathcal{C}}} \mathscr {F}$ can be defined more generally when $\mathscr {F}: \operatorname{\mathcal{C}}^{\operatorname{op}} \rightarrow \mathbf{Cat}$ is a lax functor of $2$-categories. We will return to this point in § (see Definition ).

Remark 5.5.2.5. Let $\operatorname{\mathcal{C}}$ be a category and let $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \mathbf{Cat}$ be a functor of $2$-categories. Then the construction $(C \in \operatorname{\mathcal{C}}) \mapsto \mathscr {F}(C)^{\operatorname{op}}$ determines a functor of $2$-categories $\mathscr {F}^{\operatorname{op}}: \operatorname{\mathcal{C}}= (\operatorname{\mathcal{C}}^{\operatorname{op}})^{\operatorname{op}} \rightarrow \mathbf{Cat}$. In this case, we have a canonical isomorphism of categories

\[ \int ^{ \operatorname{\mathcal{C}}^{\operatorname{op}} }(\mathscr {F}^{\operatorname{op}} ) \simeq ( \int _{\operatorname{\mathcal{C}}} \mathscr {F})^{\operatorname{op}}, \]

where the left hand side is given by Definition 5.5.2.3 and the right hand side is given by Definition 5.5.2.1.

Example 5.5.2.6 (Set-Valued Functors). Let $\operatorname{\mathcal{C}}$ be a category and let $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{Set}$ be a functor from $\operatorname{\mathcal{C}}$ to the category of sets. Then we can also regard $\mathscr {F}$ as a functor from $\operatorname{\mathcal{C}}$ to the $2$-category $\mathbf{Cat}$ (by composing with the fully faithful embedding $\operatorname{Set}\hookrightarrow \mathbf{Cat}$, carrying each set $S$ to the associated discrete category). In this case, the category $\int _{\operatorname{\mathcal{C}}} \mathscr {F}$ of Definition 5.5.2.1 agrees with the category of elements of $\mathscr {F}$ defined in Construction 5.5.1.1. Similarly, for every functor $\mathscr {F}: \operatorname{\mathcal{C}}^{\operatorname{op}} \rightarrow \operatorname{Set}$, the category $\int ^{\operatorname{\mathcal{C}}} \mathscr {F}$ can be identified with the category of elements of $\mathscr {F}$ defined in Variant 5.5.1.2.

Example 5.5.2.7. Let $\mathscr {I}$ denote the inclusion from the ordinary category $\operatorname{Cat}$ (regarded as a $2$-category having only identity $2$-morphisms) to the $2$-category $\mathbf{Cat}$, and let $\operatorname{Cat}_{\ast }^{\mathrm{lax}}$ denote the category of elements $\int _{\operatorname{Cat}} \mathscr {I}$. The category $\operatorname{Cat}_{\ast }^{\mathrm{lax}}$ can be described concretely as follows:

  • The objects of $\operatorname{Cat}_{\ast }^{\mathrm{lax}}$ are pairs $(\operatorname{\mathcal{C}}, X)$, where $\operatorname{\mathcal{C}}$ is a category and $X$ is an object of $\operatorname{\mathcal{C}}$.

  • A morphism from $(\operatorname{\mathcal{C}}, X)$ to $(\operatorname{\mathcal{D}}, Y)$ is a pair $(F, u)$, where $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ is a functor and $u: F(X) \rightarrow Y$ is a morphism in the category $\operatorname{\mathcal{D}}$.

  • If $(F,u): (\operatorname{\mathcal{C}}, X) \rightarrow (\operatorname{\mathcal{D}}, Y)$ and $(G,v): (\operatorname{\mathcal{D}}, Y) \rightarrow (\operatorname{\mathcal{E}}, Z)$ are morphisms in $\operatorname{Cat}_{\ast }^{\mathrm{lax}}$, then their composition is the pair $(G \circ F, w)$, where $w$ is the morphism of $\operatorname{\mathcal{E}}$ given by the composition

    \[ (G \circ F)(X) \xrightarrow { G(u) } G(Y) \xrightarrow {v} Z. \]

Notation 5.5.2.8. Let $\operatorname{\mathcal{C}}$ be a category and let $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \mathbf{Cat}$ be a functor of $2$-categories. Then the category of elements $\int _{\operatorname{\mathcal{C}}} \mathscr {F}$ is equipped with a forgetful functor $U: \int _{\operatorname{\mathcal{C}}} \mathscr {F} \rightarrow \operatorname{\mathcal{C}}$, given on objects by the construction $(C,X) \mapsto C$ and on morphisms by the construction $(f,u) \mapsto f$. Similarly, for every functor of $2$-categories $\mathscr {F}: \operatorname{\mathcal{C}}^{\operatorname{op}} \rightarrow \mathbf{Cat}$, the category of $\int ^{\operatorname{\mathcal{C}}} \mathscr {F}$ of Definition 5.5.2.3 is equipped with a forgetful functor $U: \int ^{\operatorname{\mathcal{C}}} \mathscr {F} \rightarrow \operatorname{\mathcal{C}}$.

Remark 5.5.2.9 (Fibers of the Forgetful Functor). Let $\operatorname{\mathcal{C}}$ be a category and let $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \mathbf{Cat}$ be a functor of $2$-categories. For every object $C \in \operatorname{\mathcal{C}}$, there is a canonical isomorphism of categories

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

which carries each object $X \in \mathscr {F}(C)$ to the object $(C,X) \in \int _{\operatorname{\mathcal{C}}} \mathscr {F}$ and each morphism $u: X \rightarrow Y$ in $\mathscr {F}$ to the morphism $(\operatorname{id}_{C}, u \circ \epsilon _{C}(X)): (C,X) \rightarrow (C,Y)$ of $\int _{\operatorname{\mathcal{C}}} \mathscr {F}$ (here $\epsilon _{C}: \mathscr {F}(\operatorname{id}_ C) \simeq \operatorname{id}_{ \mathscr {F}(C)}$ denotes the identity constraint on the functor $\mathscr {F}$). Similarly, for each functor $\mathscr {F}: \operatorname{\mathcal{C}}^{\operatorname{op}} \rightarrow \mathbf{Cat}$, we have a canonical isomorphism

\[ \mathscr {F}(C) \simeq \{ C\} \times _{ \operatorname{\mathcal{C}}} \int ^{\operatorname{\mathcal{C}}} \mathscr {F}. \]

Remark 5.5.2.10. Let $V: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$ be a functor between categories. If $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \mathbf{Cat}$ is a functor of $2$-categories, then the composition $(\mathscr {F} \circ V ): \operatorname{\mathcal{D}}\rightarrow \mathbf{Cat}$ is also a functor of $2$-categories, and we have a pullback diagram of categories

\[ \xymatrix@R =50pt@C=50pt{ \int _{\operatorname{\mathcal{D}}}( \mathscr {F} \circ V ) \ar [r] \ar [d] & \int ^{\operatorname{\mathcal{C}}} \mathscr {F} \ar [d] \\ \operatorname{\mathcal{D}}\ar [r]^-{V} & \operatorname{\mathcal{C}}} \]

where the vertical maps are the forgetful functors of Notation 5.5.2.8. Similarly, for every functor of $2$-categories $\mathscr {F}: \operatorname{\mathcal{C}}^{\operatorname{op}} \rightarrow \mathbf{Cat}$, we have a pullback diagram

\[ \xymatrix@R =50pt@C=50pt{ \int ^{\operatorname{\mathcal{D}}}( \mathscr {F} \circ V^{\operatorname{op}} ) \ar [r] \ar [d] & \int ^{\operatorname{\mathcal{C}}} \mathscr {F} \ar [d] \\ \operatorname{\mathcal{D}}\ar [r]^-{V} & \operatorname{\mathcal{C}}. } \]

Example 5.5.2.11. Let $\operatorname{\mathcal{C}}$ be a category and let $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{Cat}$ be a functor between ordinary categories, which we can identify with a strict functor from $\operatorname{\mathcal{C}}$ to the $2$-category $\mathbf{Cat}$. Applying Remark 5.5.2.10, we deduce that the category of elements $\int _{\operatorname{\mathcal{C}}} \mathscr {F}$ fits into a pullback diagram

\[ \xymatrix@R =50pt@C=50pt{ \int _{\operatorname{\mathcal{C}}} \mathscr {F} \ar [d] \ar [r] & \operatorname{Cat}_{\ast }^{\mathrm{lax}} \ar [d] \\ \operatorname{\mathcal{C}}\ar [r]^-{\mathscr {F}} & \operatorname{Cat}. } \]

Proposition 5.5.2.12. 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}}$ denote the forgetful functor. Then a morphism $(f,u): (C,X) \rightarrow (D,Y)$ of $\int _{\operatorname{\mathcal{C}}} \mathscr {F}$ is $U$-cocartesian if and only if $u: \mathscr {F}(f)(X) \rightarrow Y$ is an isomorphism in the category $\mathscr {F}(D)$.

Proof. Assume first that $u$ is an isomorphism; we wish to show that $(f,u)$ is a $U$-cocartesian morphism of the category $\int _{\operatorname{\mathcal{C}}} \mathscr {F}$. Fix a morphism $g: D \rightarrow E$ of $\operatorname{\mathcal{C}}$ and an object $Z \in \mathscr {F}(E)$; we wish to show that every morphism $(g \circ f,w): (C,X) \rightarrow (E,Z)$ in the category $\int _{\operatorname{\mathcal{C}}} \mathscr {F}$ can be written uniquely as a composition $(g,v) \circ (f,u)$ for some morphism $(g,v): (D,Y) \rightarrow (E,Z)$. Unwinding the definitions, we wish to show that there is a unique morphism $v: \mathscr {F}(g)(Y) \rightarrow Z$ in the category $\mathscr {F}(E)$ for which the composition

\[ \mathscr {F}( g \circ f)(X) \xrightarrow { \mu _{g,f}^{-1}(X) } (\mathscr {F}(g) \circ \mathscr {F}(f))(X) \xrightarrow { \mathscr {F}(g)(u) } \mathscr {F}(g)(Y) \xrightarrow {v} Z \]

is equal to $w$. This is clear, since $\mu _{g,f}^{-1}(X)$ and $\mathscr {F}(g)(u)$ are isomorphisms.

Now suppose that $(f,u)$ is a $U$-cocartesian morphism of the category $\int _{\operatorname{\mathcal{C}}} \mathscr {F}$; we wish to show that $u$ is an isomorphism. Let $\iota : \mathscr {F}(D) \rightarrow \{ D\} \times _{\operatorname{\mathcal{C}}} \int _{\operatorname{\mathcal{C}}} \mathscr {F}$ be the isomorphism of Remark 5.5.2.9. Then the morphism $(f,u)$ factors as a composition

\[ (C,X) \xrightarrow { (f,\operatorname{id}) } (D, \mathscr {F}(f)(X)) \xrightarrow { \iota (u) } (D,Y). \]

The first half of the argument shows that the morphism $(f, \operatorname{id})$ is also $U$-cocartesian, so that $\iota (u)$ is an isomorphism in the fiber $\{ D\} \times _{\operatorname{\mathcal{C}}} \int _{\operatorname{\mathcal{C}}} \mathscr {F}$. Since $\iota $ is an isomorphism of categories, it follows that $u$ is an isomorphism in the category $\mathscr {F}(D)$. $\square$

Corollary 5.5.2.13. Let $\operatorname{\mathcal{C}}$ be a category. If $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \mathbf{Cat}$ is a functor of $2$-categories, then the forgetful functor $U: \int _{\operatorname{\mathcal{C}}} \mathscr {F} \rightarrow \operatorname{\mathcal{C}}$ is a cocartesian fibration of categories. If $\mathscr {F}: \operatorname{\mathcal{C}}^{\operatorname{op}} \rightarrow \mathbf{Cat}$ is a functor of $2$-categories, then the forgetful functor $\int ^{\operatorname{\mathcal{C}}} \mathscr {F} \rightarrow \operatorname{\mathcal{C}}$ is a cartesian fibration of categories.

Proof. We will prove the first assertion; the second follows by a similar argument. Let $(C,X)$ be an object of the category $\int _{\operatorname{\mathcal{C}}} \mathscr {F}$ and let $f: C \rightarrow D$ be a morphism in $\operatorname{\mathcal{C}}$; we wish to show that $f$ can be lifted to a $U$-cocartesian morphism $(f,u): (C,X) \rightarrow (D,Y)$ of $\int _{\operatorname{\mathcal{C}}} \mathscr {F}$. This follows immediately from the criterion of Proposition 5.5.2.12: for example, we can take $Y = \mathscr {F}(f)(X)$ and $u$ to be the identity morphism. $\square$

Remark 5.5.2.14. In §5.6, we will prove a converse to Corollary 5.5.2.13: for every cocartesian fibration of categories $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$, there exists a functor of $2$-categories $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \mathbf{Cat}$ and an isomorphism of categories $\int _{\operatorname{\mathcal{C}}} \mathscr {F} \simeq \operatorname{\mathcal{E}}$ whose composition with $U$ is the forgetful functor of Notation 5.5.2.8. See Proposition 5.6.5.1.

Remark 5.5.2.15 (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.5.2.8. 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.5.2.9. 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.0.2.