# Kerodon

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

Construction 2.2.5.1 (Composition of Lax Functors). Let $\operatorname{\mathcal{C}}$, $\operatorname{\mathcal{D}}$, and $\operatorname{\mathcal{E}}$ be $2$-categories, and suppose we are given a pair of lax functors $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ and $G: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{E}}$. We define a lax functor $GF: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{E}}$ as follows:

• On objects, the lax functor $GF$ is given by $(GF)(X) = G( F(X) )$.

• For every pair of objects $X,Y \in \operatorname{\mathcal{C}}$, the functor

$(GF)_{X,Y}: \underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}( X, Y ) \rightarrow \underline{\operatorname{Hom}}_{\operatorname{\mathcal{E}}}( (GF)(X), (GF)(Y) )$

is given by the composition of functors

$\underline{ \operatorname{Hom}}_{\operatorname{\mathcal{C}}}(X,Y) \xrightarrow { F_{X,Y} } \underline{\operatorname{Hom}}_{\operatorname{\mathcal{D}}}( F(X), F(Y) ) \xrightarrow { G_{F(X), F(Y)} } \underline{\operatorname{Hom}}_{\operatorname{\mathcal{E}}}( (GF)(X), (GF)(Y) ).$

In other words, the lax functor $GF$ is given on $1$-morphisms and $2$-morphisms by the formulae

$(GF)(f) = G( F(f) ) \quad \quad (GF)( \gamma ) = G( F( \gamma ) ).$
• For each object $X \in \operatorname{\mathcal{C}}$, the identity constraint $\epsilon _{X}^{GF}: \operatorname{id}_{ (GF)(X)} \Rightarrow (GF)(\operatorname{id}_ X)$ is given by the composition

$\operatorname{id}_{(GF)(X)} \xRightarrow { \epsilon ^{G}_{F(X)} } G( \operatorname{id}_{F(X)} ) \xRightarrow { G( \epsilon ^{F}_{X} ) } (GF)(\operatorname{id}_ X).$
• For every pair of composable $1$-morphisms $X \xrightarrow {f} Y \xrightarrow {g} Z$ in the $2$-category $\operatorname{\mathcal{C}}$, the composition constraint $\mu _{g,f}^{GF}: (GF)(g) \circ (GF)(f) \rightarrow (GF)( g \circ f )$ is given by the composition

$(GF)(g) \circ (GF)(f) \xRightarrow { \mu ^{G}_{F(g), F(f)} } G( F(g) \circ F(f) ) \xRightarrow { G( \mu ^{F}_{g,f} ) } (GF)( g \circ f).$

We will refer to $GF$ as the composition of $F$ with $G$, and will sometimes denote it by $G \circ F$.