Kerodon

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

Corollary 2.2.1.15. Let $\operatorname{\mathcal{C}}$ be a $2$-category and let $X$ be an object of $\operatorname{\mathcal{C}}$. Then the left and right unit constraints

\[ \lambda _{ \operatorname{id}_ X }: \operatorname{id}_ X \circ \operatorname{id}_ X \xRightarrow {\sim } \operatorname{id}_ X \quad \quad \rho _{ \operatorname{id}_ X}: \operatorname{id}_ X \circ \operatorname{id}_ X \xRightarrow {\sim } \operatorname{id}_ X \]

are both equal to the unit constraint $\upsilon _ X: \operatorname{id}_ X \circ \operatorname{id}_{X} \xRightarrow {\sim } \operatorname{id}_ X$.

Proof. For any $1$-morphism $f: Y \rightarrow X$ in $\operatorname{\mathcal{C}}$, the left unit constraint $\lambda _{f}$ is characterized by the commutativity of the diagram

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

Using Proposition 2.2.1.14, we deduce that $\upsilon _{X} \circ \operatorname{id}_ f = \rho _{ \operatorname{id}_ X } \circ \operatorname{id}_ f$ as $2$-morphisms from $( \operatorname{id}_{X} \circ \operatorname{id}_{X} ) \circ f$ to $\operatorname{id}_{X} \circ f$. In other words, the $2$-morphisms $\upsilon _{X}, \rho _{ \operatorname{id}_ X }: \operatorname{id}_{X} \circ \operatorname{id}_{X} \Rightarrow \operatorname{id}_ X$ have the same image under the functor

\[ \underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(X,X ) \rightarrow \underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(Y,X) \quad \quad g \mapsto g \circ f. \]

In the special case where $Y = X$ and $f = \operatorname{id}_{X}$, this functor is fully faithful. It follows that $\upsilon _{X} = \rho _{ \operatorname{id}_ X }$. The equality $\upsilon _{X} = \lambda _{ \operatorname{id}_ X }$ follows by a similar argument. $\square$