Corollary commrig_ideals' (R : commrig) : lideal R ≃ rideal R. Proof. apply weqfibtototal; intro; apply commrig_ideals. Defined.
Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.MoreFoundations.Notations.