{A B} {f g : A $-> B} {A' B'} {f' g' : A' $-> B'} (a : A $-> A') (b : B $-> B') (p : f' $o a $== b $o f) (q : g' $o a $== b $o g) : ab_coeq f g $-> ab_coeq f' g'. Proof. snrapply ab_coeq_rec. 1: exact (ab_coeq_in $o b). refine (cat_assoc _ _ _ $@ _ $@ cat_assoc_opp _ _ _). refine ((_ $@L p^$) $@ _ $@ (_ $@L q)). refine (cat_assoc_opp _ _ _ $@ (_ $@R a) $@ cat_assoc _ _ _). nrapply ab_coeq_glue. Defined.
Require Import Basics Types. Require Import WildCat HSet Truncations.Core Modalities.ReflectiveSubuniverse. Require Import Groups.QuotientGroup AbelianGroup Biproduct.