Definition abmonoidshomabmonoid (X Y : abmonoid) : abmonoid. Proof. use make_abmonoid. - use make_setwithbinop. + use make_hSet. * exact (monoidfun X Y). * exact (isasetmonoidfun X Y). + intros f g. exact (abmonoidshombinop f g). - exact (abmonoidshomabmonoid_isabmonoid X Y). Defined.
Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.Algebra.Monoids2.