Lemma isasetmonoidfun (X Y : monoid) : isaset (monoidfun X Y). Proof. apply (isasetsubset (pr1monoidfun X Y)). - change (isofhlevel 2 (X → Y)). apply impred. intro. apply (setproperty Y). - refine (isinclpr1 _ _). intro. apply isapropismonoidfun. Defined.
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets.