{A : Group} {B : AbGroup} (f g : A $-> B) : A $-> B. Proof. refine (grp_homo_compose ab_codiagonal _). exact (grp_prod_corec f g). Defined.
Require Import Basics Types. Require Import WildCat HSet Truncations.Core Modalities.ReflectiveSubuniverse. Require Import Groups.QuotientGroup AbelianGroup Biproduct.