Definition 2

Let G, $G'$ be groupoids and let $\varphi$ be a morphism from G into $G'$. An inverse up to homotopy of $\varphi$ is a groupoid morphism $\psi$ from $G'$ into G such that the morphisms $\psi \circ \varphi$ and $\varphi \circ \psi$ are respectively homotopic to Id$_G$ and to Id$_{G'}$. One says that $\varphi$ is a homotopism if there exists an inverse of $\varphi$ up to homotopy.

An isomorphism of groupoids is a homotopism.

Let G and $G'$ be groupoids. Let $\varphi ,\varphi '$ be groupoid morphisms from G into $G'$ which are homotopic. If $\varphi$ is a homotopism, the same is true of $\varphi '$. In fact, if $\psi$ denotes an inverse of $\varphi$ up to homotopy, one has $\psi \circ \varphi '\sim \psi \circ \varphi \sim$ Id$_G$ and $\varphi '\circ \psi \sim \varphi \circ \psi \sim$ Id$_{G'}$, which proves that $\psi$ is an inverse up to homotopy of $\varphi '$.

Let G, $G',G''$ be groupoids and let $\varphi : G\rightarrow G',\varphi ': G'\rightarrow G''$, $\psi : G'\rightarrow G,\psi ': G''\rightarrow G'$ be groupoid morphisms. Then, of the following conditions:

(i) $\psi$ is an inverse up to homotopy of $\varphi$;

(ii) $\psi '$ is an inverse up to homotopy of $\varphi '$;

(iii) $\psi \circ \psi '$ is an inverse up to homotopy of $\varphi '\circ \varphi$; any two imply the third. In fact, suppose first that (i) and (ii) are satisfied; one then has

$\psi \circ \psi '\circ \varphi '\circ \varphi \sim \psi \circ$ Id$_{G'}\circ \varphi \sim \psi \circ \varphi \sim$ Id$_G$

and, analogously, $\varphi '\circ \varphi \circ \psi \circ \psi '\sim$ Id$_{G'}$, whence (iii). If (i) and (iii) are satisfied,

$\varphi '\circ \psi '\sim \varphi '\circ \varphi \circ \psi \circ \psi '\sim$ Id$_{G''}$

and

$\psi '\circ \varphi '\sim (\varphi \circ \psi )\circ \psi '\circ \varphi '\circ (\varphi \circ \psi )\sim \varphi \circ \psi \sim$ Id$_{G'}$,

whence condition (ii). The proof that conditions (ii) and (iii) imply condition (i) is analogous.

In particular, if two of the morphisms $\varphi ,\varphi ',\varphi '\circ \varphi$ are homotopisms, the same is true of the third.