Definition ringquot {X : ring} (R : @ringeqrel X) : ring := @make_ring (setwith2binopquot R) (isringquot R).
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.