{A B} {f g : A $-> B} : ab_coeq_in (f:=f) (g:=g) $o f $== ab_coeq_in $o g. Proof. intros x. nrapply qglue. apply tr. by exists x. Defined.
Require Import Basics Types. Require Import WildCat HSet Truncations.Core Modalities.ReflectiveSubuniverse. Require Import Groups.QuotientGroup AbelianGroup Biproduct.