Lemma isapropistwobinopfun {X Y : setwith2binop} (f : X → Y) : isaprop (istwobinopfun f). 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.