# Kerodon

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

Proposition 2.2.7.2. Let $\operatorname{\mathcal{C}}$ be a $2$-category. Then $\operatorname{\mathcal{C}}$ is strictly unitary if and only if the following conditions are satisfied:

$(a)$

For each $1$-morphism $f: X \rightarrow Y$ in $\operatorname{\mathcal{C}}$, we have $\operatorname{id}_{Y} \circ f = f = f \circ \operatorname{id}_{X}$.

$(b)$

For each object $X$ of $\operatorname{\mathcal{C}}$, the unit constraint $\upsilon _{X}: \operatorname{id}_{X} \circ \operatorname{id}_{X} \xRightarrow {\sim } \operatorname{id}_ X$ is the identity morphism from $\operatorname{id}_{X} \circ \operatorname{id}_{X} = \operatorname{id}_{X}$ to itself.

$(c)$

For every $1$-morphism $f: X \rightarrow Y$ in $\operatorname{\mathcal{C}}$, the associativity constraints $\alpha _{ \operatorname{id}_{Y}, \operatorname{id}_{Y}, f}$ and $\alpha _{ f, \operatorname{id}_ X, \operatorname{id}_ X}$ are equal to the identity (as $2$-morphisms from $f$ to itself).

Proof. If $\operatorname{\mathcal{C}}$ is strictly unitary, then $(a)$ is clear and $(b)$ follows from Corollary 2.2.1.15. Assume that $(a)$ and $(b)$ are satisfied. For any $1$-morphism $f: X \rightarrow Y$ in $\operatorname{\mathcal{C}}$, the left unit constraint $\lambda _{f}$ is characterized by the commutativity of the diagram

$\xymatrix@R =50pt@C=50pt{ \operatorname{id}_{Y} \circ ( \operatorname{id}_ Y \circ f) \ar@ {=>}[rr]^{ \alpha _{ \operatorname{id}_ Y, \operatorname{id}_ Y, f} } \ar@ {=>}[dr]_{ \operatorname{id}_{\operatorname{id}_ Y} \circ \lambda _ f} & & (\operatorname{id}_ Y \circ \operatorname{id}_ Y) \circ f \ar@ {=>}[dl]^{ \upsilon _ Y \circ \operatorname{id}_ f} \\ & \operatorname{id}_ Y \circ f, & }$

and is therefore the identity $2$-morphism if and only if $\alpha _{\operatorname{id}_ Y, \operatorname{id}_ Y, f}$ is an identity $2$-morphism (from $f$ to itself). Similarly, the right unit constraint $\rho _{f}$ is an identity $2$-morphism if and only if $\alpha _{ f, \operatorname{id}_ X, \operatorname{id}_ X }$ is an identity $2$-morphism in $\operatorname{\mathcal{C}}$. $\square$