Kerodon

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

Definition 2.2.8.17. Let $\operatorname{\mathcal{C}}$ be a $2$-category. We say that a $1$-morphism $f: X \rightarrow Y$ in $\operatorname{\mathcal{C}}$ is an isomorphism if the homotopy class $[f]$ is an isomorphism in the homotopy category $\operatorname{hPith}(\operatorname{\mathcal{C}})$. Equivalently, $f$ is an isomorphism if there exists another $1$-morphism $g: Y \rightarrow X$ such that $g \circ f$ and $f \circ g$ are isomorphic to $\operatorname{id}_{X}$ and $\operatorname{id}_{Y}$ as objects of the categories $\underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(X,X)$ and $\underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(Y,Y)$, respectively. In this case, $g$ is also an isomorphism in $\operatorname{\mathcal{C}}$, which we will refer to as a homotopy inverse to $f$.