`{Funext} (A : Group) (B : AbGroup) : Group. Proof. nrefine (Build_Group (GroupHomomorphism A B) ab_homo_add grp_homo_const negate_hom _). repeat split. 1: exact _. all: hnf; intros; apply equiv_path_grouphomomorphism; intro; cbn. + apply associativity. + apply left_identity. + apply right_identity. + apply left_inverse. + apply right_inverse. Defined.
Require Import Basics Types. Require Import WildCat HSet Truncations.Core Modalities.ReflectiveSubuniverse. Require Import Groups.QuotientGroup AbelianGroup Biproduct.