{A B f g} (P : @ab_coeq A B f g -> Type) `{forall x, IsHProp (P x)} (i : forall b, P (ab_coeq_in b)) : forall x, P x. Proof. rapply Quotient_ind_hprop. exact i. Defined.
Require Import Basics Types. Require Import WildCat HSet Truncations.Core Modalities.ReflectiveSubuniverse. Require Import Groups.QuotientGroup AbelianGroup Biproduct.