proposition: Lemma isasetbinopfun (X Y : setwithbinop) : isaset (binopfun X Y).
proof: Proof. apply (isasetsubset (pr1binopfun X Y)). - change (isofhlevel 2 (X -> Y)). apply impred. intro. apply (setproperty Y). - refine (isinclpr1 _ _). intro. apply isapropisbinopfun. Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions