Lemma isasettwobinopfun (X Y : setwith2binop) : isaset (twobinopfun X Y). Proof. apply (isasetsubset (pr1twobinopfun X Y)). - change (isofhlevel 2 (X → Y)). apply impred. intro. apply (setproperty Y). - refine (isinclpr1 _ _). intro. apply isapropistwobinopfun. Qed.