Lemma isapropismonoidfun {X Y : monoid} (f : X → Y) : isaprop (ismonoidfun f). Proof. apply isofhleveldirprod. - apply isapropisbinopfun. - apply (setproperty Y). Defined.
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets.