fact: Definition Abel_rec (P : Type) `{IsHSet P} (a : G -> P) (c : forall x y z, a (x * (y * z)) = a (x * (z * y))) : Abel -> P.
imports: Basics Types Truncations.Core Cubical WildCat Colimits.Coeq Algebra.Groups.Group Algebra.AbGroups.AbelianGroup Modalities.ReflectiveSubuniverse