Kerodon

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

Remark 6.1.4.3. Let $\operatorname{\mathcal{C}}$ be a $2$-category and let $f: C \rightarrow D$ be a $1$-morphism of $\operatorname{\mathcal{C}}$. By definition, $f$ is an isomorphism if and only if there exists a $1$-morphism $g: D \rightarrow C$ together with isomorphisms

\[ \eta : \operatorname{id}_{C} \xRightarrow {\sim } g \circ f \quad \quad \epsilon : f \circ g \xRightarrow {\sim } \operatorname{id}_{D} \]

in the categories $\underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(C,C)$ and $\underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(D,D)$, respectively. The main content of Proposition 6.1.4.1 is that, if such isomorphisms exist, then we can choose $\eta $ and $\epsilon $ to be compatible in the sense that they satisfy conditions $(Z1)$ and $(Z2)$ of Definition 6.1.1.1. Note that in this case, $\eta $ is determined by $\epsilon $ and vice versa (Proposition 6.1.2.9).