Definition setwith2binop_univalence_weq2 (X Y : setwith2binop) : (X ╝ Y) ≃ (twobinopiso X Y). Proof. use weqbandf. - use hSet_univalence. - intros e. use invweq. induction X as [X Xop]. induction Y as [Y Yop]. cbn in e. induction e. use weqimplimpl. + intros i. use dirprod_paths. * use funextfun. intros x1. use funextfun. intros x2. exact ((dirprod_pr1 i) x1 x2). * use funextfun. intros x1. use funextfun. intros x2. exact ((dirprod_pr2 i) x1 x2). + intros e. cbn in e. use make_istwobinopfun. * intros x1 x2. induction e. use idpath. * intros x1 x2. induction e. use idpath. + use isapropistwobinopfun. + use isasettwobinoponhSet. Defined.