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