Definition opposite_ring (X : ring) : ring. Proof. refine (pr1 (X⁰),, _). split. - split. apply make_isabgrop. * exact (pr1 (rigop1axs (X⁰)),, pr2 (pr1 (ringop1axs X))). * exact (pr2 (ringop1axs X)). * exact (rigop2axs (X⁰)). - exact (rigdistraxs (X⁰)). Defined.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.