proposition: Lemma isasettwobinopfun (X Y : setwith2binop) : isaset (twobinopfun X Y).
proof: Proof. apply (isasetsubset (pr1twobinopfun X Y)). - change (isofhlevel 2 (X -> Y)). apply impred. intro. apply (setproperty Y). - refine (isinclpr1 _ _). intro. apply isapropistwobinopfun. Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions