Definition rig_univalence_weq2 (X Y : rig) : (X ╝ Y) ≃ (rigiso' X Y). Proof. use weqbandf. - exact (setwith2binop_univalence X Y). - intros e. cbn. use invweq. induction X as [X Xop]. induction Y as [Y Yop]. cbn in e. cbn. induction e. use weqimplimpl. + intros i. use proofirrelevance. use isapropisrigops. + intros i. now induction i. + use isapropdirprod. * use setproperty. * use setproperty. + use isapropifcontr. exact (@isapropisrigops X op1 op2 Xop Yop). Defined.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.