Question about the definition of Group

[anotherArka]

Somebody has defined a data type group as

data Group: (g: Type) -> Type where
MkGroup: (grp : Type) -> (() : grp -> grp -> grp) -> (IsGroup grp ()) -> Group grp

What is the reason behind adding this definition?
It makes the code slightly more complicated, though that's not a big issue. But defining an additional data type might just create some internal error. But sometimes definitions using constructors creates some problems. Although I don't know when it will create a problem.