# Kerodon

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

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$