Definition abmonoid_of_monoid (X : monoid) (H : iscomm (@op X)) : abmonoid := make_abmonoid X (make_isabmonoidop (pr2 X) H).
Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.Algebra.Monoids2.