Lemma isasetbinopfun (X Y : setwithbinop) : isaset (binopfun X Y). Proof. apply (isasetsubset (pr1binopfun X Y)). - change (isofhlevel 2 (X → Y)). apply impred. intro. apply (setproperty Y). - refine (isinclpr1 _ _). intro. apply isapropisbinopfun. Defined.