{A B} {f g : A $-> B} : B $-> ab_coeq f g. Proof. snrapply grp_quotient_map. Defined.
Require Import Basics Types. Require Import WildCat HSet Truncations.Core Modalities.ReflectiveSubuniverse. Require Import Groups.QuotientGroup AbelianGroup Biproduct.