proposition: Lemma isasetmonoidfun (X Y : monoid) : isaset (monoidfun X Y).
proof: Proof. apply (isasetsubset (pr1monoidfun X Y)). - change (isofhlevel 2 (X -> Y)). apply impred. intro. apply (setproperty Y). - refine (isinclpr1 _ _). intro. apply isapropismonoidfun. Defined.
imports: UniMath.Algebra.BinaryOperations UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders