nLab [defines a strict 2-groups](https://ncatlab.org/nlab/show/strict+2-group) in many different but equivalent ways, among them:


* an internal group object in Cat,
* an internal group object in Grpd


Also, it is known that strict 2-groups may be defined from crossed modules (see for example [Baez](http://arxiv.org/abs/1003.4485)). There is one thing I don't understand (I will consider the 2-group as a 2-category by the delooping process of the monoidal category that we obtain by one or the other of definitions):


* Seeing a 2-group as internal to Cat or to Grpd will give, at first glance slightly different structures, the difference is being that the second internalization will make 2-morphisms vertically invertible, but not the first one.
* Constructing a 2-group from a crossed-module (as done in the reference) will also make 2-morphisms vertically invertible.


Hence, I see that only when we define a 2-group as a group internal to Cat the 2-morphisms are not (a least directly) defined as vertically invertible. I suspect the functoriality of the group multiplication functor to be responsible for defining vertical inverses (**this turned out to be false**) but I do not see how! My question: how to prove that each 2-morphism of a 2-group (s̲e̲e̲n̲ ̲a̲s̲ ̲a̲ ̲g̲r̲o̲u̲p̲ ̲o̲b̲j̲e̲c̲t̲ ̲i̲n̲ ̲C̲a̲t̲) has a vertical inverse, knowing that the vertical composition is inherited from the category composition law in the object of Cat that, unlike an object in Grpd, does not define canonically inverses .



strict 2-groups VS crossed modules
Let us prove the analogous claim for weak 2-groups (this implies, in particular, the strict case). Let $\mathcal{C}$ be a monoidal category with unit $\mathbb{I} \in \mathcal{C}$. 


**Claim**: Suppose there exists a functor $Inv: \mathcal{C} \to \mathcal{C}$ and natural isomorphisms $\psi\_X: \mathbb{I} \stackrel{\cong}{\to} X \otimes Inv(X)$ and $\phi\_X: Inv(X) \otimes X \stackrel{\cong}{\to} \mathbb{I}$. Then $\mathcal{C}$ is a groupoid.


**Proof:**
Let $f: X \to Y$ be a map in $\mathcal{C}$. We need to show that $f$ is an isomorphism. Let $g: Y \to X$ be the composed map
$$ Y \stackrel{\psi\_X \otimes Id\_Y}{\to} X \otimes Inv(X) \otimes Y \stackrel{Id\_X \otimes Inv(f) \otimes Id\_Y}{\to} X \otimes Inv(Y) \otimes Y \stackrel{Id\_X \otimes \phi\_Y}{\to} X $$
We now claim that $g \circ f$ is an isomorphism. Indeed, $g \circ f$ is equal to the composition
$$ X \stackrel{\psi\_X \otimes Id\_X}{\to} X \otimes Inv(X) \otimes X \stackrel{Id\_X \otimes Inv(f) \otimes f}{\to} X \otimes Inv(Y) \otimes Y \stackrel{Id\_X \otimes \phi\_Y}{\to} X $$
and the naturality of $\phi$ implies that $Inv(f) \otimes f$ is an isomorphism. A similar argument shows that $f \circ g$ is an isomoprhism. It follows that both $f$ and $g$ are isomorphisms.


