proposition: Theorem ab_pushout_rec {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: 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^ @ _). unfold uncurry; cbn. refine (ap011 sg_op (preserves_negate _) (p a)^ @ _). exact (left_inverse _). Defined.
imports: Basics Types Truncations.Core Modalities.ReflectiveSubuniverse WildCat.Core HSet Algebra.Groups.Image Algebra.Groups.QuotientGroup AbGroups.AbelianGroup AbGroups.Biproduct