{A B : AbGroup} {f g : A $-> B} {C : AbGroup} (i : B $-> C) (p : i $o f $== i $o g) : ab_coeq f g $-> C. Proof. snrapply (grp_quotient_rec _ _ i). cbn. intros b H. strip_truncations. destruct H as [a q]. destruct q; simpl. lhs nrapply grp_homo_op. lhs nrapply (ap (.* _)). 1: apply grp_homo_inv. apply grp_moveL_M1^-1. exact (p a)^. Defined.
Require Import Basics Types. Require Import WildCat HSet Truncations.Core Modalities.ReflectiveSubuniverse. Require Import Groups.QuotientGroup AbelianGroup Biproduct.