Definition isabmonoidquot {X : abmonoid} (R : binopeqrel X) : isabmonoidop (@op (setwithbinopquot R)) := ismonoidquot R ,, iscommquot R.
Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.Algebra.Monoids2.