Lemma isaset_ideal : isaset ideal. Proof. apply isaset_total2. - apply isaset_submonoid. - intro S. apply isasetaprop, propproperty. Defined.
Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.MoreFoundations.Notations.