Definition ismonoidquot {X : monoid} (R : binopeqrel X) : ismonoidop (@op (setwithbinopquot R)) := isassocquot R ,, setquotpr R (pr1 (pr2 (pr2 X))) ,, isunitquot R.
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets.