{G : Group} {A : AbGroup} (f : G $-> A) : abel G $-> A. Proof. snrapply Build_GroupHomomorphism. { srapply (Abel_rec _ _ f). intros x y z. nrapply grp_homo_op_agree; trivial. refine (grp_homo_op _ _ _ @ _ @ (grp_homo_op _ _ _)^). apply commutativity. } intros y. Abel_ind_hprop x; revert y. Abel_ind_hprop y. apply grp_homo_op. 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.