{A B C : AbGroup} (f : A $-> B) (g : A $-> C) : Subgroup (ab_biprod B C) := grp_image (ab_biprod_corec (ab_homo_negation $o f) g).
Require Import Basics Types Truncations.Core. Require Import WildCat.Core HSet. Require Import AbGroups.AbelianGroup AbGroups.Biproduct.