Kerodon

Proof. We proceed as in the proof of Proposition 5.6.1.3, with some minor variations in notation. 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}(Y) )$, where $\epsilon _{D}: \operatorname{id}_{ \mathscr {F}(D) } \rightarrow \mathscr {F}( \operatorname{id}_{D} )$ is the identity constraint for the lax 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: X \rightarrow \mathscr {F}(f)(Y)$ is equal to the composition

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

  This follows from the observation that the composite transformation

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

  is the identity, which follows from axiom $(b)$ 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: Y \rightarrow \mathscr {F}(g)(Z)$ is given by the upper cycle in the diagram

  \[ \xymatrix@R =50pt@C=50pt{ Y \ar [r]^-{ \epsilon _{D}(Y) } \ar [d]^-{v} & \mathscr {F}(\operatorname{id}_ D)(Y) \ar [d]^-{ \mathscr {F}(\operatorname{id}_ D)(v) } & \\ \mathscr {F}(v)(Z) \ar [r]^-{\epsilon _ D( \mathscr {F}(v)(Z) )} & (\mathscr {F}(\operatorname{id}_ D) \circ \mathscr {F}(v))(Z) \ar [r]^-{ \mu _{\operatorname{id}_{D}, v)}(Z)} & \mathscr {F}(v)(Z). } \]

  Since $\epsilon _{D}$ is a natural transformation, this diagram commutes. It will therefore suffice to show that the lower composition is equal to $v$, which follows from axiom $(a)$ 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}(e) \circ \mathscr {F}(f))(Y) \rightarrow \mathscr {F}(g \circ f \circ e)(Z)$ are the morphisms in the category $\mathscr {F}(B)$ given by clockwise and counterclockwise composition in the diagram

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