Kerodon

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

Remark 2.2.1.13 (Naturality of Unit Constraints). Let $\operatorname{\mathcal{C}}$ be a $2$-category, let $X$ and $Y$ be objects of $\operatorname{\mathcal{C}}$, and let $\gamma : f \Rightarrow g$ be a morphism in the category $\underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(X,Y)$. Then the diagram of $2$-morphisms

\[ \xymatrix { \operatorname{id}_{Y} \circ f \ar@ {=>}[r]^{ \lambda _ f } \ar@ {=>}[d]^{ \operatorname{id}_{\operatorname{id}_ Y} \circ \gamma } & f \ar@ {=>}[d]^{\gamma } \\ \operatorname{id}_{Y} \circ g \ar@ {=>}[r]^{ \lambda _ g } & g } \]

commutes. In other words, the construction $f \mapsto \lambda _{f}$ determines a natural isomorphism from the functor

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

to the identity functor. Similarly, the construction $f \mapsto \rho _{f}$ determines a natural isomorphism from the functor

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

to the identity functor.