Definition monoidquotpr {X : monoid} (R : binopeqrel X) : monoidfun X (monoidquot R) := monoidfunconstr (ismonoidfun_setquotpr R).
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets.