`{Funext} (A : Group) (B : AbGroup) : AbGroup. Proof. snrapply (Build_AbGroup (grp_hom A B)). intros f g; cbn. apply equiv_path_grouphomomorphism; intro x; cbn. apply commutativity. Defined.
Require Import Basics Types. Require Import WildCat HSet Truncations.Core Modalities.ReflectiveSubuniverse. Require Import Groups.QuotientGroup AbelianGroup Biproduct.