Kerodon

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

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$.