{A B C : AbGroup} (f : A $-> B) (g : A $-> C) (Y : AbGroup) : {b : B $-> Y & {c : C $-> Y & b o f == c o g}} -> (ab_pushout f g $-> Y). Proof. intros [b [c p]]; exact (ab_pushout_rec b c p). Defined.
Require Import Basics Types Truncations.Core. Require Import WildCat.Core HSet. Require Import AbGroups.AbelianGroup AbGroups.Biproduct.