{A B C : AbGroup} {f : A $-> B} {g : A $-> C} : B $-> ab_pushout f g := grp_quotient_map $o grp_prod_inl.
Require Import Basics Types Truncations.Core. Require Import WildCat.Core HSet. Require Import AbGroups.AbelianGroup AbGroups.Biproduct.