Kerodon

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}: \operatorname{id}_{ \mathscr {F}(D) } \xrightarrow {\sim } \mathscr {F}( \operatorname{id}_{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}(f)(X) \ar [d]^-{u} \ar [r]^-{ \epsilon _{D}(\mathscr {F}(f)(X)) }_-{\sim } & (\mathscr {F}(\operatorname{id}_ D) \circ \mathscr {F}(f))(X) \ar [d]^-{ \mathscr {F}(\operatorname{id}_ D)(u) } & \\ Y \ar [r]^-{ \epsilon _{D}(Y) }_-{\sim } & \mathscr {F}(\operatorname{id}_ D)(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

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

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

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$