Definition ismonoidfuntoabgrdiff (X : abmonoid) : ismonoidfun (toabgrdiff X) := isbinopfuntoabgrdiff X ,, isunitalfuntoabgrdiff X.
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Subtypes.