Definition ringconstr {X : hSet} (opp1 opp2 : binop X) (ax11 : isgrop opp1) (ax12 : iscomm opp1) (ax2 : ismonoidop opp2) (dax : isdistr opp1 opp2) : ring := @make_ring (make_setwith2binop X (opp1 ,, opp2)) (((ax11 ,, ax12) ,, ax2) ,, dax).
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.