Definition setwithbinopdirprod (X Y : setwithbinop) : setwithbinop. Proof. exists (setdirprod X Y). unfold binop. simpl. apply (λ xy xy' : X × Y, op (pr1 xy) (pr1 xy') ,, op (pr2 xy) (pr2 xy')). Defined.