proposition: Proposition ab_pushout_rec_beta `{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: 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_beta' (phi $o grp_quotient_map) bc). Defined.
imports: Basics Types Truncations.Core Modalities.ReflectiveSubuniverse WildCat.Core HSet Algebra.Groups.Image Algebra.Groups.QuotientGroup AbGroups.AbelianGroup AbGroups.Biproduct