Kerodon

Definition 2.2.6.1. Let $\operatorname{\mathcal{C}}$ and $\operatorname{\mathcal{D}}$ be $2$-categories. We will say that a functor $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ is an isomorphism if it is an isomorphism in the category $\operatorname{2Cat}$ of Definition 2.2.5.5. That is, $F$ is an isomorphism if there exists a functor $G: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$ such that $GF = \operatorname{id}_{\operatorname{\mathcal{C}}}$ and $FG = \operatorname{id}_{\operatorname{\mathcal{C}}}$. We say that $2$-categories $\operatorname{\mathcal{C}}$ and $\operatorname{\mathcal{D}}$ are isomorphic if there exists an isomorphism from $\operatorname{\mathcal{C}}$ to $\operatorname{\mathcal{D}}$.