Kerodon

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

Construction 2.2.1.11 (Left and Right Unit Constraints). Let $\operatorname{\mathcal{C}}$ be a $2$-category. For every $1$-morphism $f: X \rightarrow Y$ in $\operatorname{\mathcal{C}}$, we have canonical isomorphisms

\[ \operatorname{id}_{Y} \circ (\operatorname{id}_{Y} \circ f) \xRightarrow {\alpha _{\operatorname{id}_ Y, \operatorname{id}_ Y, f} } (\operatorname{id}_{Y} \circ \operatorname{id}_{Y} ) \circ f \xRightarrow { \upsilon _{Y} \circ \operatorname{id}_{f} } \operatorname{id}_{Y} \circ f. \]

Since composition on the left with $\operatorname{id}_{Y}$ is fully faithful, it follows that there is a unique isomorphism $\lambda _{f}: \operatorname{id}_{Y} \circ f \xRightarrow {\sim } f$ for which 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} }_{\sim } \ar@ {=>}[dr]_{ \operatorname{id}_{\operatorname{id}_ Y} \circ \lambda _ f }^{\sim } & & (\operatorname{id}_ Y \circ \operatorname{id}_ Y) \circ f \ar@ {=>}[dl]^{ \upsilon _ Y \circ \operatorname{id}_ f}_{\sim } \\ & \operatorname{id}_ Y \circ f & } \]

commutes. We will refer to $\lambda _{f}$ as the left unit constraint. Similarly, there is a unique isomorphism $\rho _{f}: f \circ \operatorname{id}_{X} \xRightarrow {\sim } f$ for which the diagram

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

commutes; we refer to $\rho _ f$ as the right unit constraint.