{R : Ring} (X : R -> Type) : Ideal R. Proof. snrapply Build_Ideal; [|split]. - snrapply Build_Subgroup'. + exact (fun x => merely (ideal_generated_type X x)). + exact _. + apply tr, igt_zero. + intros x y p q; strip_truncations. by apply tr, igt_add_neg. - intros r x; apply Trunc_functor. nrapply igt_mul_l. - intros x r; apply Trunc_functor. nrapply igt_mul_r. Defined.
Require Import Basics Types. Require Import Spaces.Finite.Fin. Require Import Classes.interfaces.canonical_names. Require Import Algebra.Rings.Ring. Require Import Algebra.Groups.Subgroup. Require Import Algebra.AbGroups. Require Import WildCat.Core. Module Import Notation.