fact: Definition group_precomp {a b} := @cat_precomp Group _ _ a b.
imports: Basics Types Truncations.Core Cubical WildCat Colimits.Coeq Algebra.Groups.Group Algebra.AbGroups.AbelianGroup Modalities.ReflectiveSubuniverse