# Kerodon

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

Proposition 2.2.7.7. Let $\operatorname{\mathcal{C}}$ be a $2$-category. Then there exists a strictly unitary isomorphism $\operatorname{\mathcal{C}}\simeq \operatorname{\mathcal{C}}'$, where $\operatorname{\mathcal{C}}'$ is a strictly unitary $2$-category.

Proof. Let $\mu = \{ \mu _{g,f} \}$ be the twisting cochain on $\operatorname{\mathcal{C}}$ given on composable $1$-morphisms $X \xrightarrow {f} Y \xrightarrow {g} Z$ by the formula

$\mu _{g,f} = \begin{cases} \lambda ^{-1}_{f}: f \Rightarrow g \circ f & \text{ if } g = \operatorname{id}_{Y} \\ \rho ^{-1}_{g}: g \Rightarrow g \circ f & \text{ if } f = \operatorname{id}_ Y \\ \operatorname{id}_{g \circ f}: g \circ f \Rightarrow g \circ f & \text{ otherwise. } \end{cases}$

Note that this prescription is consistent, since $\lambda _{f} = \upsilon _{Y} = \rho _{g}$ in the special case where $f = \operatorname{id}_ Y = g$ (Corollary 2.2.1.15). Let $\operatorname{\mathcal{C}}'$ be the twist of $\operatorname{\mathcal{C}}$ with respect to the cocycle $\{ \mu _{g,f} \}$ (Construction 2.2.6.8). Then $\operatorname{\mathcal{C}}'$ is a strictly unitary $2$-category (in the sense of Definition 2.2.7.1), and Exercise 2.2.6.9 supplies a strictly unitary isomorphism of $2$-categories $\operatorname{\mathcal{C}}\simeq \operatorname{\mathcal{C}}'$ $\square$