proposition: Lemma ab_biprod_corec_diagonal `{Funext} {A B : AbGroup} (f g : B $-> A) : ab_biprod_corec f g = (functor_ab_biprod f g) $o ab_diagonal.
proof: Proof. apply equiv_path_grouphomomorphism; reflexivity. Defined.
imports: Basics Types Truncations.Core WildCat HSet AbelianGroup Modalities.ReflectiveSubuniverse