(P : Type) `{IsHSet P} (a : G -> P) (c : forall x y z, a (x * (y * z)) = a (x * (z * y))) : Abel -> P. Proof. apply (Abel_ind _ a). intros; apply dp_const, c. Defined.
Require Import Basics Types Truncations.Core. Require Import Cubical.DPath WildCat. Require Import Colimits.Coeq. Require Import Algebra.AbGroups.AbelianGroup. Require Import Modalities.ReflectiveSubuniverse.