Definition rigconstr {X : hSet} (opp1 opp2 : binop X) (ax11 : ismonoidop opp1) (ax12 : iscomm opp1) (ax2 : ismonoidop opp2) (m0x : ∏ x : X, opp2 (unel_is ax11) x = unel_is ax11) (mx0 : ∏ x : X, opp2 x (unel_is ax11) = unel_is ax11) (dax : isdistr opp1 opp2) : rig. Proof. intros. exists (make_setwith2binop X (opp1 ,, opp2)). split. - exists ((ax11 ,, ax12) ,, ax2). apply (m0x ,, mx0). - apply dax. Defined.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.