proposition: Lemma isapropistwobinopfun {X Y : setwith2binop} (f : X -> Y) : isaprop (istwobinopfun f).
proof: Proof. apply isofhleveldirprod. - apply impred. intro x. apply impred. intro x'. apply (setproperty Y). - apply impred. intro x. apply impred. intro x'. apply (setproperty Y). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions