Definition isabmonoidcarrier {X : abmonoid} (A : submonoid X) : isabmonoidop (@op A) := ismonoidcarrier A ,, iscommcarrier A.
Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.Algebra.Monoids2.