`{Funext} {A B C Y : AbGroup} {f : A $-> B} {g : A $-> C} (phi : ab_pushout f g $-> Y) : ab_pushout_rec (phi $o ab_pushout_inl) (phi $o ab_pushout_inr) (fun a:A => ap phi (ab_pushout_commsq a)) = phi. Proof. rapply (equiv_ap' (equiv_quotient_abgroup_ump (G:=ab_biprod B C) _ Y)^-1%equiv _ _)^-1. srapply path_sigma_hprop. refine (grp_quotient_rec_beta _ Y _ _ @ _). apply equiv_path_grouphomomorphism; intro bc. exact (ab_biprod_rec_eta (phi $o grp_quotient_map) bc). Defined.
Require Import Basics Types Truncations.Core. Require Import WildCat.Core HSet. Require Import AbGroups.AbelianGroup AbGroups.Biproduct.