{A B C f g} {l r : @ab_coeq A B f g $-> C} (p : l $o ab_coeq_in $== r $o ab_coeq_in) : l $== r. Proof. srapply ab_coeq_ind_hprop. exact p. Defined.
Require Import Basics Types. Require Import WildCat HSet Truncations.Core Modalities.ReflectiveSubuniverse. Require Import Groups.QuotientGroup AbelianGroup Biproduct.