Definition subabmonoid_incl {X : abmonoid} (A : subabmonoid X) : monoidfun A X := submonoid_incl A.
Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.Algebra.Monoids2.