{A B C Y : AbGroup} {f : A $-> B} {g : A $-> C} (b : B $-> Y) (c : C $-> Y) (p : b o f == c o g) : ab_pushout f g $-> Y. Proof. srapply grp_quotient_rec. - exact (ab_biprod_rec b c). - intros [x y] q; strip_truncations; simpl. destruct q as [a q]. cbn in q. refine (ap (uncurry (fun x y => b x + c y)) q^ @ _). cbn. refine (ap011 sg_op (preserves_negate _) (p a)^ @ _). exact (left_inverse _). Defined.
Require Import Basics Types Truncations.Core. Require Import WildCat.Core HSet. Require Import AbGroups.AbelianGroup AbGroups.Biproduct.