# Kerodon

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

Proposition 2.2.1.16. Let $\operatorname{\mathcal{C}}$ be a $2$-category containing a pair of composable $1$-morphisms $f: X \rightarrow Y$ and $g: Y \rightarrow Z$. Then:

$(1)$

The associativity constraint $\alpha _{\operatorname{id}_ Z,g,f}: \operatorname{id}_{Z} \circ (g \circ f) \Rightarrow (\operatorname{id}_ Z \circ g) \circ f$ is given by the (vertical) composition

$\operatorname{id}_{Z} \circ (g \circ f) \xRightarrow { \lambda _{g \circ f} } g \circ f \xRightarrow {\lambda ^{-1}_{g} \circ \operatorname{id}_{f} } (\operatorname{id}_ Z \circ g) \circ f.$
$(2)$

The associativity constraint $\alpha _{g,f,\operatorname{id}_ X}: g \circ (f \circ \operatorname{id}_ X) \Rightarrow (g \circ f) \circ \operatorname{id}_ X$ is given by the (vertical) composition

$g \circ (f \circ \operatorname{id}_ X) \xRightarrow { \operatorname{id}_{g} \circ \rho _{f}} g \circ f \xRightarrow { \rho ^{-1}_{g \circ f} } (g \circ f) \circ \operatorname{id}_ X$

Proof of Proposition 2.2.1.16. We will prove $(2)$; the proof of $(1)$ is similar. Set $e = \operatorname{id}_ X$, and consider the diagram of isomorphisms

$\xymatrix@C =0pt@R=40pt{ & g \circ ((f \circ e) \circ e) \ar@ {=>}[rr]^{ \alpha _{g, f \circ e, e} } \ar@ {=>}[d]^-{\rho _ f} & & (g \circ (f \circ e)) \circ e \ar@ {=>}[dr]^{ \alpha _{g, f, e} } \ar@ {=>}[dl]_-{\rho _ f} & \\ g \circ (f \circ (e \circ e) ) \ar@ {=>}[ur]^{ \alpha _{f,e,e} } \ar@ {=>}[drr]_{ \alpha _{g,f,e \circ e}} \ar@ {=>}[r]^-{\lambda _ e} & g \circ (f \circ e) \ar@ {=>}[r]^-{\alpha _{g,f,e}} & (g \circ f) \circ e & & ((g \circ f) \circ e) \circ e \ar@ {=>}[ll]_-{\rho _{g \circ f}} \\ & & (g \circ f) \circ (e \circ e). \ar@ {=>}[urr]_{\alpha _{ g \circ f, e, e} } \ar@ {=>}[u]_-{\lambda _ e } & & }$

Here the outer cycle of the diagram commutes by the pentagon identity for $\operatorname{\mathcal{C}}$, the triangles on the upper left and lower right commute by virtue of Proposition 2.2.1.14, and the upper and lower square diagrams commute by the functoriality of the associativity constraints. It follows that the triangle on the upper right commutes: that is, the identity $\alpha _{g,f,\operatorname{id}_ X} = \rho ^{-1}_{g \circ f} (\operatorname{id}_ g \circ \rho _{f} )$ holds after applying the functor $(\bullet \circ \operatorname{id}_ X): \underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(X,Z) \rightarrow \underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(X,Z)$. Since this functor is an equivalence of categories (it is isomorphic to the identity functor by means of the right unit constraint $\rho$), we conclude that the identity $\alpha _{g,f,\operatorname{id}_ X} = \rho _{g \circ f}^{-1} (\operatorname{id}_ g \circ \rho _{f} )$ holds in $\underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(X,Z)$ itself. $\square$