Definition monoidquot {X : monoid} (R : binopeqrel X) : monoid. Proof. exists (setwithbinopquot R). apply ismonoidquot. Defined.
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets.