nLab defines a strict 2-groups 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). 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 .