Definition setwithbinop_univalence_weq2 (X Y : setwithbinop) : (X ╝ Y) ≃ (binopiso 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 funextfun. intros x1. use funextfun. intros x2. exact (i x1 x2). + intros e. cbn in e. intros x1 x2. induction e. use idpath. + use isapropisbinopfun. + use isasetbinoponhSet. Defined.