diff --git a/theories/Algebra/Groups/Commutator.v b/theories/Algebra/Groups/Commutator.v
index 2ad6a3e5ae..89c623dc67 100644
--- a/theories/Algebra/Groups/Commutator.v
+++ b/theories/Algebra/Groups/Commutator.v
@@ -1,5 +1,5 @@
 Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc
-  Basics.Iff Basics.Equivalences.
+  Basics.Iff Basics.Equivalences Basics.Predicate.
 Require Import Types.Sigma Types.Paths.
 Require Import Groups.Group AbGroups.Abelianization AbGroups.AbelianGroup
   Groups.QuotientGroup.
@@ -228,7 +228,7 @@ Local Open Scope group_scope.
 (** [subgroup_commutator H K] is the smallest subgroup containing the commutators of elements of [H] with elements of [K]. *)
 Definition subgroup_commutator_rec {G : Group} {H K : Subgroup G} (J : Subgroup G)
   (i : forall x y, H x -> K y -> J (grp_commutator x y))
-  : forall x, [H, K] x -> J x.
+  : pred_subset [H, K] J.
 Proof.
   rapply subgroup_generated_rec; intros x [[y Hy] [[z Kz] p]];
     destruct p; simpl.
@@ -239,7 +239,7 @@ Defined.
 Definition subgroup_commutator_2_rec {G : Group} {H J K : Subgroup G}
   (N : Subgroup G) `{!IsNormalSubgroup N}
   (i : forall x y z, H x -> J y -> K z -> N (grp_commutator (grp_commutator x y) z))
-  : forall x, [[H, J], K] x -> N x.
+  : pred_subset [[H, J], K] N.
 Proof.
   snapply subgroup_commutator_rec.
   intros x z HJx Kz; revert x HJx.
@@ -259,27 +259,26 @@ Defined.
 
 (** Commutator subgroups are functorial. *)
 Definition functor_subgroup_commutator {G : Group} {H J K L : Subgroup G}
-  (f : forall x, H x -> K x) (g : forall x, J x -> L x)
-  : forall x, [H, J] x -> [K, L] x.
+  (f : pred_subset H K) (g : pred_subset J L)
+  : pred_subset [H, J] [K, L].
 Proof.
   snapply subgroup_commutator_rec.
   intros x y Hx Jx.
-  apply subgroup_commutator_in.
-  - by apply f.
-  - by apply g.
+  exact (subgroup_commutator_in (f _ Hx) (g _ Jx)).
 Defined.
 
 Definition subgroup_eq_commutator {G : Group} {H J K L : Subgroup G}
-  (f : forall x, H x <-> K x) (g : forall x, J x <-> L x)
-  : forall x, [H, J] x <-> [K, L] x.
+  (f : pred_eq H K) (g : pred_eq J L)
+  : pred_eq [H, J] [K, L].
 Proof.
-  intros x; split; revert x; apply functor_subgroup_commutator.
-  1,3: apply f.
-  1,2: apply g.
+  snapply pred_subset_antisymm; apply functor_subgroup_commutator.
+  3,4: apply pred_eq_subset'.
+  1,3: exact f.
+  1,2: exact g.
 Defined.
 
 Definition subgroup_incl_commutator_symm {G : Group} (H J : Subgroup G)
-  : forall x, [H, J] x -> [J, H] x.
+  : pred_subset [H, J] [J, H].
 Proof.
   snapply subgroup_commutator_rec.
   intros x y Hx Jy.
@@ -290,15 +289,14 @@ Defined.
 
 (** Commutator subgroups are symmetric in their arguments. *)
 Definition subgroup_commutator_symm {G : Group} (H J : Subgroup G)
-  : forall x, [H, J] x <-> [J, H] x.
+  : pred_eq [H, J] [J, H].
 Proof.
-  intros x; split; snapply subgroup_incl_commutator_symm.
+  snapply pred_subset_antisymm; apply subgroup_incl_commutator_symm.
 Defined.
 
 (** The opposite subgroup of a commutator subgroup is the commutator subgroup of the opposite subgroups. *)
 Definition subgroup_eq_commutator_grp_op {G : Group} (H J : Subgroup G)
-  : forall (x : grp_op G), [H, J] x
-    <-> [subgroup_grp_op J, subgroup_grp_op H] x.
+  : pred_eq (subgroup_grp_op [H, J]) [subgroup_grp_op J, subgroup_grp_op H].
 Proof.
   napply (subgroup_eq_subgroup_generated_op (G:=G)).
   intro x.
@@ -338,7 +336,7 @@ Defined.
 (** Commutator subgroups distribute over products of normal subgroups on the left. *)
 Definition subgroup_commutator_normal_prod_l {G : Group}
   (H K L : NormalSubgroup G)
-  : forall x, [subgroup_product H K, L] x <-> subgroup_product [H, L] [K, L] x.
+  : pred_eq [subgroup_product H K, L] (subgroup_product [H, L] [K, L]).
 Proof.
   intros x; split.
   - revert x; snapply subgroup_commutator_rec.
@@ -354,17 +352,19 @@ Proof.
   - revert x; snapply subgroup_generated_rec.
     intros x [HLx | KLx].
     + revert x HLx.
-      apply functor_subgroup_commutator; trivial.
+      apply functor_subgroup_commutator.
+      2: reflexivity.
       apply subgroup_product_incl_l.
     + revert x KLx.
-      apply functor_subgroup_commutator; trivial.
+      apply functor_subgroup_commutator.
+      2: reflexivity.
       apply subgroup_product_incl_r.
 Defined.
 
 (** Commutator subgroups distribute over products of normal subgroups on the right. *)
 Definition subgroup_commutator_normal_prod_r {G : Group}
   (H K L : NormalSubgroup G)
-  : forall x, [H, subgroup_product K L] x <-> subgroup_product [H, K] [H, L] x.
+  : pred_eq [H, subgroup_product K L] (subgroup_product [H, K] [H, L]).
 Proof.
   intros x.
   etransitivity.
@@ -378,11 +378,11 @@ Defined.
 (** The subgroup image of a commutator is included in the commutator of the subgroup images. The converse only generally holds for a normal [J] and [K] and a surjective [f]. *)
 Definition subgroup_image_commutator_incl {G H : Group}
   (f : G $-> H) (J K : Subgroup G)
-  : forall x, subgroup_image f [J, K] x
-    -> [subgroup_image f J, subgroup_image f K] x.
+  : pred_subset
+      (subgroup_image f [J, K])
+      [subgroup_image f J, subgroup_image f K].
 Proof.
   snapply subgroup_image_rec.
-  change ([?G, ?H] (f ?x)) with (subgroup_preimage f [G, H] x).
   snapply subgroup_commutator_rec.
   intros x y Jx Ky.
   change (subgroup_preimage f [?G, ?H] ?x) with ([G, H] (f x)).
@@ -447,9 +447,9 @@ Defined.
 
 Definition three_subgroups_lemma (G : Group) (H J K N : Subgroup G)
   `{!IsNormalSubgroup N}
-  (T1 : forall x, [[H, J], K] x -> N x)
-  (T2 : forall x, [[J, K], H] x -> N x)
-  : forall x, [[K, H], J] x -> N x.
+  (T1 : pred_subset [[H, J], K] N)
+  (T2 : pred_subset [[J, K], H] N)
+  : pred_subset [[K, H], J] N.
 Proof.
   rapply subgroup_commutator_2_rec.
   Local Close Scope group_scope.
diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v
index 73e4c4046f..441485ce7f 100644
--- a/theories/Algebra/Groups/Subgroup.v
+++ b/theories/Algebra/Groups/Subgroup.v
@@ -826,6 +826,10 @@ Proof.
   exact (tr (sgt_op p q)).
 Defined.
 
+Definition subgroup_generated_in {G : Group} {X : G -> Type}
+  : pred_subset X (subgroup_generated X)
+  := fun _ => (tr o sgt_in).
+
 (** The inclusion of generators into the generated subgroup. *)
 Definition subgroup_generated_gen_incl {G : Group} {X : G -> Type} (g : G) (H : X g)
   : subgroup_generated X
@@ -833,8 +837,8 @@ Definition subgroup_generated_gen_incl {G : Group} {X : G -> Type} (g : G) (H :
 
 (** The generated subgroup is the smallest subgroup containing the generating set. *)
 Definition subgroup_generated_rec {G : Group} (X : G -> Type) (S : Subgroup G)
-  (i : forall g, X g -> S g)
-  : forall g, subgroup_generated X g -> S g.
+  (i : pred_subset X S)
+  : pred_subset (subgroup_generated X) S.
 Proof.
   intros g; rapply Trunc_rec; intros p.
   induction p as [g Xg | | g h p1 IHp1 p2 IHp2].
@@ -844,37 +848,40 @@ Proof.
 Defined.
 
 (** If [f : G $-> H] is a group homomorphism and [X] and [Y] are subsets of [G] and [H] such that [f] maps [X] into [Y], then [f] sends the subgroup generated by [X] into the subgroup generated by [Y]. *)
-Definition functor_subgroup_generated {G H : Group} (X : G -> Type) (Y : H -> Type)
-  (f : G $-> H) (preserves : forall g, X g -> Y (f g))
-  : forall g, subgroup_generated X g -> subgroup_generated Y (f g).
+Definition functor_subgroup_generated {G H : Group}
+  (X : G -> Type) (Y : H -> Type) (f : G $-> H) (preserves : pred_subset X (Y o f))
+  : pred_subset (subgroup_generated X) (subgroup_generated Y o f).
 Proof.
-  change (subgroup_generated Y (f ?g))
-    with (subgroup_preimage f (subgroup_generated Y) g).
-  apply subgroup_generated_rec.
-  intros g p.
-  apply tr, sgt_in.
-  by apply preserves.
+  apply (subgroup_generated_rec _ (subgroup_preimage f (subgroup_generated Y))).
+  transitivity (Y o f).
+  1: apply preserves.
+  apply (pred_subset_precomp f).
+  apply subgroup_generated_in.
 Defined.
 
+Definition functor_subgroup_generated' {G : Group}
+  (X : G -> Type) (Y : G -> Type) (preserves : pred_subset X Y)
+  : pred_subset (subgroup_generated X) (subgroup_generated Y)
+  := functor_subgroup_generated X Y (Id _) preserves.
+
 Definition subgroup_eq_functor_subgroup_generated {G H : Group}
-  (X : G -> Type) (Y : H -> Type) (f : G $<~> H) (preserves : forall g, X g <-> Y (f g))
-  : forall g, subgroup_generated X g <-> subgroup_generated Y (f g).
+  (X : G -> Type) (Y : H -> Type) (f : G $<~> H) (preserves : pred_eq X (Y o f))
+  : pred_eq (subgroup_generated X) (subgroup_generated Y o f).
 Proof.
-  intros x; split; revert x.
+  apply pred_subset_antisymm.
   - apply functor_subgroup_generated.
-    apply preserves.
-  - equiv_intro f^-1$ x.
-    rewrite eisretr.
-    apply functor_subgroup_generated; clear x.
-    equiv_intro f x; intros y.
-    simpl; rewrite (eissect f).
-    by apply preserves.
+    exact preserves.
+  - apply (pred_subset_moveR_equiv f).
+    apply (functor_subgroup_generated _ _ f^-1$).
+    apply (pred_subset_moveL_equiv f).
+    apply pred_eq_subset.
+    by symmetry.
 Defined.
 
 (** A similar result is true if we replace one group by its opposite, i.e. if [f] is an anti-homomorphism.  For simplicity, we state this only for the case in which [f] is the identity isomorphism.  It's also useful in the special case where [X] and [Y] are the same. *)
 Definition subgroup_eq_subgroup_generated_op {G : Group}
-  (X : G -> Type) (Y : G -> Type) (preserves : forall g, X g <-> Y g)
-  : forall g, subgroup_generated X g <-> subgroup_generated (G:=grp_op G) Y g.
+  (X : G -> Type) (Y : G -> Type) (preserves : pred_eq X Y)
+  : pred_eq (subgroup_generated X) (subgroup_generated (G:=grp_op G) Y).
 Proof.
   intro g; split.
   1: change (subgroup_generated X g -> subgroup_grp_op (subgroup_generated (G:=grp_op G) Y) g).
@@ -894,8 +901,8 @@ Definition subgroup_product {G : Group} (H K : Subgroup G) : Subgroup G
 (** The induction principle for the product. *)
 Definition subgroup_product_ind {G : Group} (H K : Subgroup G)
   (P : forall x, subgroup_product H K x -> Type)
-  (P_H_in : forall x y, P x (tr (sgt_in (inl y))))
-  (P_K_in : forall x y, P x (tr (sgt_in (inr y))))
+  (P_H_in : forall x y, P x (subgroup_generated_in _ (inl y)))
+  (P_K_in : forall x y, P x (subgroup_generated_in _ (inr y)))
   (P_unit : P mon_unit (tr sgt_unit))
   (P_op : forall x y h k, P x (tr h) -> P y (tr k) -> P (x * - y) (tr (sgt_op h k)))
   `{forall x y, IsHProp (P x y)}
@@ -912,12 +919,12 @@ Proof.
 Defined.
 
 Definition subgroup_product_incl_l {G : Group} (H K : Subgroup G)
-  : forall x, H x -> subgroup_product H K x
-  := fun x => tr o sgt_in o inl.
+  : pred_subset H (subgroup_product H K)
+  := fun x => subgroup_generated_in _ o inl.
 
 Definition subgroup_product_incl_r {G : Group} (H K : Subgroup G)
-  : forall x, K x -> subgroup_product H K x
-  := fun x => tr o sgt_in o inr.
+  : pred_subset K (subgroup_product H K)
+  := fun x => subgroup_generated_in _ o inr.
 
 (** A product of normal subgroups is normal. *)
 Instance isnormal_subgroup_product {G : Group} (H K : Subgroup G)
@@ -937,8 +944,8 @@ Definition normalsubgroup_product {G : Group} (H K : NormalSubgroup G)
 
 Definition functor_subgroup_product {G H : Group}
   {J K : Subgroup G} {L M : Subgroup H}
-  (f : G $-> H) (l : forall x, J x -> L (f x)) (r : forall x, K x -> M (f x))
-  : forall x, subgroup_product J K x -> subgroup_product L M (f x).
+  (f : G $-> H) (l : pred_subset J (L o f)) (r : pred_subset K (M o f))
+  : pred_subset (subgroup_product J K) (subgroup_product L M o f).
 Proof.
   snapply functor_subgroup_generated.
   exact (fun x => functor_sum (l x) (r x)).
@@ -947,15 +954,16 @@ Defined.
 Definition subgroup_eq_functor_subgroup_product {G H : Group}
   {J K : Subgroup G} {L M : Subgroup H}
   (f : G $<~> H) (l : forall x, J x <-> L (f x)) (r : forall x, K x <-> M (f x))
-  : forall x, subgroup_product J K x <-> subgroup_product L M (f x).
+  : pred_eq (subgroup_product J K) (subgroup_product L M o f).
 Proof.
   snapply subgroup_eq_functor_subgroup_generated.
   exact (fun x => iff_functor_sum (l x) (r x)).
 Defined.
 
 Definition subgroup_eq_product_grp_op {G : Group} (H K : Subgroup G)
-  : forall x, subgroup_grp_op (subgroup_product H K) x
-    <-> subgroup_product (subgroup_grp_op H) (subgroup_grp_op K) x.
+  : pred_eq
+      (subgroup_grp_op (subgroup_product H K))
+      (subgroup_product (subgroup_grp_op H) (subgroup_grp_op K)).
 Proof.
   intro x.
   apply subgroup_eq_subgroup_generated_op.
@@ -966,9 +974,10 @@ Defined.
 
 (** This gets used twice in [path_subgroup_generated], so we factor it out here. *)
 Local Lemma path_subgroup_generated_helper {G : Group}
-  (X Y : G -> Type) (K : forall g, merely (X g) -> merely (Y g))
-  : forall g, Trunc (-1) (subgroup_generated_type X g)
-         -> Trunc (-1) (subgroup_generated_type Y g).
+  (X Y : G -> Type) (K : pred_subset (merely o X) (merely o Y))
+  : pred_subset
+      (merely o subgroup_generated_type X)
+      (merely o subgroup_generated_type Y).
 Proof.
   intro g; apply Trunc_rec; intro ing.
   induction ing as [g x| |g h Xg IHYg Xh IHYh].
@@ -980,13 +989,13 @@ Defined.
 
 (** If the predicates selecting the generators are merely equivalent, then the generated subgroups are equal. (One could probably prove that the generated subgroup are isomorphic without using univalence.) *)
 Definition path_subgroup_generated `{Univalence} {G : Group}
-  (X Y : G -> Type) (K : forall g, Trunc (-1) (X g) <-> Trunc (-1) (Y g))
+  (X Y : G -> Type) (K : pred_eq (merely o X) (merely o Y))
   : subgroup_generated X = subgroup_generated Y.
 Proof.
   rapply equiv_path_subgroup'. (* Uses Univalence. *)
-  intro g; split.
-  - apply path_subgroup_generated_helper, (fun x => fst (K x)).
-  - apply path_subgroup_generated_helper, (fun x => snd (K x)).
+  intro g; split; apply path_subgroup_generated_helper.
+  - exact K.
+  - exact (fun _ => snd (K _)).
 Defined.
 
 (** Equal subgroups have isomorphic underlying groups. *)
@@ -1071,7 +1080,7 @@ Definition subgroup_image {G H : Group} (f : G $-> H)
 
 (** By definition, values of [f x] where [x] is in a subgroup [J] are in the image of [J] under [f]. *)
 Definition subgroup_image_in {G H : Group} (f : G $-> H) (J : Subgroup G)
-  : forall x, J x -> subgroup_image f J (f x)
+  : pred_subset J (subgroup_image f J o f)
   := fun x Jx => tr ((x; Jx); idpath).
 
 (** Converting the subgroups to groups, we get the expected surjective (epi) restriction homomorphism. *)
@@ -1089,8 +1098,8 @@ Definition issurj_grp_homo_subgroup_image_in {G H : Group}
 (** An image of a subgroup [J] is included in a subgroup [K] if (and only if) [J] is included in the preimage of the subgroup [K]. *)
 Definition subgroup_image_rec {G H : Group}
   (f : G $-> H) {J : Subgroup G} {K : Subgroup H}
-  (g : forall x, J x -> K (f x))
-  : forall x, subgroup_image f J x -> K x.
+  (g : pred_subset J (subgroup_preimage f K))
+  : pred_subset (subgroup_image f J) K.
 Proof.
   intros x; apply Trunc_rec; intros [[j Jj] p].
   destruct p.
@@ -1100,8 +1109,8 @@ Defined.
 (** The image functor is adjoint to the preimage functor. *) 
 Definition iff_subgroup_image_rec {G H : Group}
   (f : G $-> H) {J : Subgroup G} {K : Subgroup H}
-  : (forall x, subgroup_image f J x -> K x)
-    <-> (forall x, J x -> subgroup_preimage f K x).
+  : pred_subset (subgroup_image f J) K
+    <-> pred_subset J (subgroup_preimage f K). 
 Proof.
   split.
   - intros rec x Jx.
diff --git a/theories/Algebra/Rings/CRing.v b/theories/Algebra/Rings/CRing.v
index cca0287f3e..fa9c998164 100644
--- a/theories/Algebra/Rings/CRing.v
+++ b/theories/Algebra/Rings/CRing.v
@@ -121,7 +121,7 @@ Section IdealCRing.
   (** Ideal products are commutative in commutative rings. Note that we are using ideal notations here and [↔] corresponds to equality of ideals. Essentially a subset in each direction. *)
   Lemma ideal_product_comm (I J : Ideal R) : I ⋅ J ↔ J ⋅ I.
   Proof.
-    apply ideal_subset_antisymm;
+    apply pred_subset_antisymm;
     apply ideal_product_subset_product_commutative.
   Defined.
   
@@ -143,7 +143,7 @@ Section IdealCRing.
   Proof.
     intros p.
     etransitivity.
-    { apply ideal_eq_subset.
+    { apply pred_eq_subset.
       symmetry.
       apply ideal_product_unit_r. }
     etransitivity.
@@ -156,7 +156,7 @@ Section IdealCRing.
     : Coprime I J -> I ∩ J ↔ I ⋅ J.
   Proof.
     intros p.
-    apply ideal_subset_antisymm.
+    apply pred_subset_antisymm.
     - apply ideal_intersection_subset_product.
       unfold Coprime in p.
       apply symmetry in p.
@@ -167,7 +167,7 @@ Section IdealCRing.
   Lemma ideal_quotient_product (I J K : Ideal R)
     : (I :: J) :: K ↔ (I :: (J ⋅ K)).
   Proof.
-    apply ideal_subset_antisymm.
+    apply pred_subset_antisymm.
     - intros x [p q]; strip_truncations; split; apply tr;
       intros r; rapply Trunc_rec; intros jk.
       + induction jk as [y [z z' j k] | | ? ? ? ? ? ? ].
diff --git a/theories/Algebra/Rings/ChineseRemainder.v b/theories/Algebra/Rings/ChineseRemainder.v
index e28f7c0ebd..38f09855d1 100644
--- a/theories/Algebra/Rings/ChineseRemainder.v
+++ b/theories/Algebra/Rings/ChineseRemainder.v
@@ -118,7 +118,7 @@ Section ChineseRemainderTheorem.
     1: exact rng_homo_crt.
     1: exact _.
     (** Finally we must show the ideal of this map is the intersection. *)
-    apply ideal_subset_antisymm.
+    apply pred_subset_antisymm.
     - intros r [i j].
       apply path_prod; apply qglue.
       1: change (I (- r + 0)).
diff --git a/theories/Algebra/Rings/Ideal.v b/theories/Algebra/Rings/Ideal.v
index f4cb211d3f..78766edfcd 100644
--- a/theories/Algebra/Rings/Ideal.v
+++ b/theories/Algebra/Rings/Ideal.v
@@ -74,6 +74,12 @@ Definition ideal_op (R : Ring) : Ideal R -> Ideal (rng_op R)
   := fun I => Build_Ideal (rng_op R) I _.
 Coercion ideal_op : Ideal >-> Ideal.
 
+Definition rightideal_op (R : Ring) : LeftIdeal R -> RightIdeal (rng_op R)
+  := idmap.
+
+Definition leftideal_op (R : Ring) : RightIdeal R -> LeftIdeal (rng_op R)
+  := idmap.
+
 (** *** Truncatedness properties *)
 
 Section IdealTrunc.
@@ -137,6 +143,38 @@ Section IdealElements.
   Definition ideal_in_plus_r : I (a + b) -> I a -> I b := subgroup_in_op_r I a b.
 End IdealElements.
 
+(** *** Ideal equality *)
+
+(** With univalence we can characterize equality of ideals. *)
+Definition equiv_path_ideal `{Univalence} {R : Ring} {I J : Ideal R}
+  : pred_eq I J <~> I = J.
+Proof.
+  refine ((equiv_ap' (issig_Ideal R)^-1 _ _)^-1 oE _).
+  refine (equiv_path_sigma_hprop _ _ oE _).
+  rapply equiv_path_subgroup'.
+Defined.
+
+(** Under funext, ideal equality is a proposition. *)
+Instance ishprop_ideal_eq `{Funext} {R : Ring} (I J : Ideal R)
+  : IsHProp (pred_eq I J) := _.
+
+(** *** Left and right ideals are invariant under ideal equality *)
+
+(** Left ideals are invariant under ideal equality. *)
+Definition isleftideal_eq {R : Ring} (I J : Subgroup R) (p : pred_eq I J)
+  : IsLeftIdeal I -> IsLeftIdeal J.
+Proof.
+  intros i r x j.
+  apply p in j.
+  apply p.
+  by apply i.
+Defined.
+
+(** Right ideals are invariant under ideal equality. *)
+Definition isrightideal_eq {R : Ring} (I J : Subgroup R) (p : pred_eq I J)
+  : IsRightIdeal I -> IsRightIdeal J
+  := isleftideal_eq (R := rng_op R) I J p.
+
 (** ** Constructions of ideals *)
 
 (** *** Zero Ideal *)
@@ -293,6 +331,13 @@ Inductive ideal_product_naive_type {R : Ring} (I J : Subgroup R) : R -> Type :=
 Definition ideal_product_type {R : Ring} (I J : Subgroup R) : Subgroup R
   := subgroup_generated (G := R) (ideal_product_naive_type I J). 
 
+(** The product ideal swapped is just the product ideal of the opposite ring. *)
+Definition ideal_product_type_op {R : Ring} (I J : Subgroup R)
+  : pred_eq (ideal_product_type (R:=R) I J) (ideal_product_type (R:=rng_op R) J I).
+Proof.
+  intros x; split; tapply (functor_subgroup_generated _ _ (Id _)); intros r []; by napply ipn_in.
+Defined.
+
 (** The product of left ideals is a left ideal. *)
 Instance isleftideal_ideal_product_type {R : Ring} (I J : Subgroup R)
   `{IsLeftIdeal R I, IsLeftIdeal R J}
@@ -311,12 +356,9 @@ Instance isrightideal_ideal_product_type {R : Ring} (I J : Subgroup R)
   `{IsRightIdeal R I, IsRightIdeal R J}
   : IsRightIdeal (ideal_product_type I J).
 Proof.
-  intro r.
-  napply (functor_subgroup_generated _ _ (grp_homo_rng_right_mult (R:=R) r)).
-  intros s [s1 s2 p1 p2]; cbn.
-  rewrite <- simple_associativity.
-  nrefine (ipn_in I J s1 (s2 * r) p1 _).
-  by apply isrightideal.
+  napply isrightideal_eq.
+  1: symmetry; rapply ideal_product_type_op.
+  by apply isleftideal_ideal_product_type.
 Defined.
 
 (** The product of ideals is an ideal. *)
@@ -335,6 +377,16 @@ Definition rightideal_product {R : Ring}
   : RightIdeal R -> RightIdeal R -> RightIdeal R
   := leftideal_product.
 
+Definition leftideal_product_op {R : Ring} (I J : RightIdeal R)
+  : leftideal_product (leftideal_op R I) (leftideal_op R J)
+    = rightideal_product I J
+  := idpath.
+
+Definition rightideal_product_op {R : Ring} (I J : LeftIdeal R)
+  : rightideal_product (rightideal_op R I) (rightideal_op R J)
+    = leftideal_product I J
+  := idpath.
+
 (** Product of ideals. *)
 Definition ideal_product {R : Ring}
   : Ideal R -> Ideal R -> Ideal R
@@ -469,63 +521,6 @@ Defined.
 Definition ideal_principal {R : Ring} (x : R) : Ideal R
   := ideal_generated (fun r => x = r).
 
-(** *** Ideal equality *)
-
-(** Classically, set based equality suffices for ideals. Since we are talking about predicates, we use pointwise iffs. This can of course be shown to be equivalent to the identity type. *)
-Definition ideal_eq {R : Ring} (I J : Subgroup R) := forall x, I x <-> J x.
-
-(** With univalence we can characterize equality of ideals. *)
-Lemma equiv_path_ideal `{Univalence} {R : Ring} {I J : Ideal R} : ideal_eq I J <~> I = J.
-Proof.
-  refine ((equiv_ap' (issig_Ideal R)^-1 _ _)^-1 oE _).
-  refine (equiv_path_sigma_hprop _ _ oE _).
-  rapply equiv_path_subgroup'.
-Defined.
-
-(** Under funext, ideal equiality is a proposition. *)
-Instance ishprop_ideal_eq `{Funext} {R : Ring} (I J : Ideal R)
-  : IsHProp (ideal_eq I J) := _.
-
-(** Ideal equality is reflexive. *)
-Instance reflexive_ideal_eq {R : Ring} : Reflexive (@ideal_eq R).
-Proof.
-  intros I x; by split.
-Defined.
-
-(** Ideal equality is symmetric. *)
-Instance symmetric_ideal_eq {R : Ring} : Symmetric (@ideal_eq R).
-Proof.
-  intros I J p x; specialize (p x); by symmetry.
-Defined.
-
-(** Ideal equality is transitive. *)
-Instance transitive_ideal_eq {R : Ring} : Transitive (@ideal_eq R).
-Proof.
-  intros I J K p q x; specialize (p x); specialize (q x); by transitivity (J x).
-Defined.
-
-(** *** Subset relation on ideals *)
-
-(** We define the subset relation on ideals in the usual way: *)
-Definition ideal_subset {R : Ring} (I J : Subgroup R) := (forall x, I x -> J x).
-
-(** The subset relation is reflexive. *)
-Instance reflexive_ideal_subset {R : Ring} : Reflexive (@ideal_subset R)
-  := fun _ _ => idmap.
-
-(** The subset relation is transitive. *)
-Instance transitive_ideal_subset {R : Ring} : Transitive (@ideal_subset R).
-Proof.
-  intros x y z p q a.
-  exact (q a o p a).
-Defined.
-
-(** We can coerce equality to the subset relation, since equality is defined to be the subset relation in each direction. *)
-Coercion ideal_eq_subset {R : Ring} {I J : Subgroup R} : ideal_eq I J -> ideal_subset I J.
-Proof.
-  intros f x; apply f.
-Defined.
-
 (** *** Quotient (a.k.a colon) ideals *)
 
 (** The definitions here are not entirely standard, but will become so when considering only commutative rings. For the non-commutative case there isn't a lot written about ideal quotients. *)
@@ -710,7 +705,7 @@ Definition ideal_annihilator {R : Ring} (I : Ideal R) : Ideal R
 
 (** Two ideals are coprime if their sum is the unit ideal. *)
 Definition Coprime {R : Ring} (I J : Ideal R) : Type
-  := ideal_eq (ideal_sum I J) (ideal_unit R).
+  := pred_eq (ideal_sum I J) (ideal_unit R).
 Existing Class Coprime.
 
 Instance ishprop_coprime `{Funext} {R : Ring}
@@ -720,7 +715,7 @@ Proof.
     exact _.
 Defined.
 
-Lemma equiv_coprime_sum `{Funext} {R : Ring} (I J : Ideal R)
+Definition equiv_coprime_sum `{Funext} {R : Ring} (I J : Ideal R)
   : Coprime I J
   <~> hexists (fun '(((i ; p) , (j ; q)) : sig I * sig J)
       => i + j = ring_one).
@@ -781,8 +776,8 @@ Defined.
 (** We declare and import a module for various (unicode) ideal notations. These exist in their own special case, and can be imported and used in other files when needing to reason about ideals. *)
 
 Module Import Notation.
-  Infix "⊆" := ideal_subset       : ideal_scope.
-  Infix "↔" := ideal_eq           : ideal_scope.
+  Infix "⊆" := pred_subset        : ideal_scope.
+  Infix "↔" := pred_eq            : ideal_scope.
   Infix "+" := ideal_sum          : ideal_scope.
   Infix "⋅" := ideal_product      : ideal_scope.
   Infix "∩" := ideal_intersection : ideal_scope.
@@ -791,431 +786,456 @@ Module Import Notation.
   Notation Ann := ideal_annihilator.
 End Notation.
 
-(** *** Ideal lemmas *)
-
-Section IdealLemmas.
-
-  Context {R : Ring}.
-
-  (** Subset relation is antisymmetric. *)
-  Lemma ideal_subset_antisymm (I J : Subgroup R) : I ⊆ J -> J ⊆ I -> I ↔ J.
-  Proof.
-    intros p q x; split; by revert x.
-  Defined.
-
-  (** The zero ideal is contained in all ideals. *)
-  Lemma ideal_zero_subset (I : Subgroup R) : ideal_zero R ⊆ I.
-  Proof.
-    intros x p; rewrite p; apply ideal_in_zero.
-  Defined.
-
-  (** The unit ideal contains all ideals. *)
-  Lemma ideal_unit_subset (I : Subgroup R) : I ⊆ ideal_unit R.
-  Proof.
-    hnf; cbn; trivial.
-  Defined.
-
-  (** Intersection includes into the left *)
-  Lemma ideal_intersection_subset_l (I J : Ideal R) : I ∩ J ⊆ I.
-  Proof.
-    intro; exact fst.
-  Defined.
-
-  (** Intersection includes into the right *)
-  Lemma ideal_intersection_subset_r (I J : Ideal R) : I ∩ J ⊆ J.
-  Proof.
-    intro; exact snd.
-  Defined.
-
-  (** Subsets of intersections *)
-  Lemma ideal_intersection_subset (I J K : Ideal R)
-    : K ⊆ I -> K ⊆ J -> K ⊆ I ∩ J.
-  Proof.
-    intros p q x r; specialize (p x r); specialize (q x r); by split.
-  Defined.
-
-  (** Ideals include into their sum on the left *)
-  Lemma ideal_sum_subset_l (I J : Ideal R) : I ⊆ (I + J).
-  Proof.
-    intros x p.
-    apply tr, sgt_in.
-    left; exact p.
-  Defined.
+(** *** Ideal Lemmas *)
 
-  (** Ideals include into their sum on the right *)
-  Lemma ideal_sum_subset_r (I J : Ideal R) : J ⊆ (I + J).
-  Proof.
-    intros x p.
-    apply tr, sgt_in.
-    right; exact p.
-  Defined.
+(** The zero ideal is contained in all ideals. *)
+Definition ideal_zero_subset {R : Ring} (I : Subgroup R) : ideal_zero R ⊆ I.
+Proof.
+  intros x p; rewrite p; apply ideal_in_zero.
+Defined.
 
-  #[local] Hint Extern 4 => progress (cbv beta iota) : typeclass_instances.
+(** The unit ideal contains all ideals. *)
+Definition ideal_unit_subset {R : Ring} (I : Subgroup R) : I ⊆ ideal_unit R.
+Proof.
+  hnf; cbn; trivial.
+Defined.
 
-  (** Products of ideals are included in their left factor *)
-  Lemma ideal_product_subset_l (I J : Ideal R) : I ⋅ J ⊆ I.
-  Proof.
-    intros r p.
-    strip_truncations.
-    induction p as [r i | | r s p1 IHp1 p2 IHp2 ].
-    + destruct i as [s t].
-      by rapply isrightideal.
-    + rapply ideal_in_zero.
-    + by rapply ideal_in_plus_negate.
-  Defined.
-
-  (** Products of ideals are included in their right factor. *)
-  Lemma ideal_product_subset_r (I J : Ideal R) : I ⋅ J ⊆ J.
-  Proof.
-    intros r p.
-    strip_truncations.
-    induction p as [r i | | r s p1 IHp1 p2 IHp2 ].
-    + destruct i as [s t].
-      by apply isleftideal.
-    + rapply ideal_in_zero.
-    + by rapply ideal_in_plus_negate.
-  Defined.
-
-  (** Products of ideals preserve subsets on the left *)
-  Lemma ideal_product_subset_pres_l (I J K : Ideal R) : I ⊆ J -> I ⋅ K ⊆ J ⋅ K.
-  Proof.
-    intros p r q.
-    strip_truncations.
-    induction q as [r i | | r s ].
-    + destruct i.
-      apply tr, sgt_in, ipn_in.
-      1: apply p.
-      1,2: assumption.
-    + apply ideal_in_zero.
-    + by apply ideal_in_plus_negate.
-  Defined.
-
-  (** Products of ideals preserve subsets on the right *)
-  Lemma ideal_product_subset_pres_r (I J K : Ideal R) : I ⊆ J -> K ⋅ I ⊆ K ⋅ J.
-  Proof.
-    intros p r q.
-    strip_truncations.
-    induction q as [r i | | r s ].
-    + destruct i.
-      apply tr, sgt_in, ipn_in.
-      2: apply p.
-      1,2: assumption.
-    + apply ideal_in_zero.
-    + by apply ideal_in_plus_negate.
-  Defined.
-
-  (** TODO: *)
-  (** The product of ideals is an associative operation. *)
-  (* Lemma ideal_product_assoc (I J K : Ideal R) : I ⋅ (J ⋅ K) ↔ (I ⋅ J) ⋅ K.
-  Proof.
-    intros r; split; exact Trunc_functor.
-  Abort. *)
-
-  (** Products of ideals are subsets of their intersection. *)
-  Lemma ideal_product_subset_intersection (I J : Ideal R) : I ⋅ J ⊆ I ∩ J.
-  Proof.
-    apply ideal_intersection_subset.
-    + apply ideal_product_subset_l.
-    + apply ideal_product_subset_r.
-  Defined.
-
-  (** Sums of ideals are the smallest ideal containing the summands. *)
-  Lemma ideal_sum_smallest (I J K : Ideal R) : I ⊆ K -> J ⊆ K -> (I + J) ⊆ K.
-  Proof.
-    intros p q.
-    refine (ideal_sum_ind I J (fun x _ => K x) p q _ _).
-    1: apply ideal_in_zero.
-    intros y z s t.
-    rapply ideal_in_plus_negate.
-  Defined.
-
-  (** Ideals absorb themselves under sum. *)
-  Lemma ideal_sum_self (I : Ideal R) : I + I ↔ I.
-  Proof.
-    apply ideal_subset_antisymm.
-    1: by rapply ideal_sum_smallest.
-    rapply ideal_sum_subset_l.
-  Defined.
-
-  (** Sums preserve inclusions in the left summand. *)
-  Lemma ideal_sum_subset_pres_l (I J K : Ideal R) : I ⊆ J -> (I + K) ⊆ (J + K).
-  Proof.
-    intros p.
-    apply ideal_sum_smallest.
-    { transitivity J.
-      1: exact p.
-      apply ideal_sum_subset_l. }
-    apply ideal_sum_subset_r.
-  Defined.
-
-  (** Sums preserve inclusions in the right summand. *)
-  Lemma ideal_sum_subset_pres_r (I J K : Ideal R) : I ⊆ J -> (K + I) ⊆ (K + J).
-  Proof.
-    intros p.
-    apply ideal_sum_smallest.
-    1: apply ideal_sum_subset_l.
-    transitivity J.
+(** Intersection includes into the left *)
+Definition ideal_intersection_subset_l {R : Ring} (I J : Ideal R) : I ∩ J ⊆ I.
+Proof.
+  intro; exact fst.
+Defined.
+
+(** Intersection includes into the right *)
+Definition ideal_intersection_subset_r {R : Ring} (I J : Ideal R) : I ∩ J ⊆ J.
+Proof.
+  intro; exact snd.
+Defined.
+
+(** Subsets of intersections *)
+Definition ideal_intersection_subset {R : Ring} (I J K : Ideal R)
+  : K ⊆ I -> K ⊆ J -> K ⊆ I ∩ J.
+Proof.
+  intros p q x r; specialize (p x r); specialize (q x r); by split.
+Defined.
+
+(** Ideals include into their sum on the left *)
+Definition ideal_sum_subset_l {R : Ring} (I J : Ideal R) : I ⊆ (I + J).
+Proof.
+  intros x p.
+  apply tr, sgt_in.
+  left; exact p.
+Defined.
+
+(** Ideals include into their sum on the right *)
+Definition ideal_sum_subset_r {R : Ring} (I J : Ideal R) : J ⊆ (I + J).
+Proof.
+  intros x p.
+  apply tr, sgt_in.
+  right; exact p.
+Defined.
+
+#[local] Hint Extern 4 => progress (cbv beta iota) : typeclass_instances.
+
+(** Products of ideals are included in their left factor *)
+Definition ideal_product_subset_l {R : Ring} (I J : Ideal R) : I ⋅ J ⊆ I.
+Proof.
+  napply subgroup_generated_rec.
+  intros _ [].
+  by rapply isrightideal.
+Defined.
+
+(** Products of ideals are included in their right factor. *)
+Definition ideal_product_subset_r {R : Ring} (I J : Ideal R) : I ⋅ J ⊆ J.
+Proof.
+  napply subgroup_generated_rec.
+  intros _ [].
+  by rapply isleftideal.
+Defined.
+
+(** Products of ideals preserve subsets on the left *)
+Definition ideal_product_subset_pres_l {R : Ring} (I J K : Ideal R)
+  : I ⊆ J -> I ⋅ K ⊆ J ⋅ K.
+Proof.
+  intros p.
+  tapply (functor_subgroup_generated _ _ (Id _)).
+  intros _ [].
+  apply ipn_in.
+  1: apply p.
+  1,2: assumption.
+Defined.
+
+(** Products of ideals preserve subsets on the right *)
+Definition ideal_product_subset_pres_r {R : Ring} (I J K : Ideal R)
+  : I ⊆ J -> K ⋅ I ⊆ K ⋅ J.
+Proof.
+  intros p.
+  tapply (functor_subgroup_generated _ _ (Id _)).
+  intros _ [].
+  apply ipn_in.
+  2: apply p.
+  1,2: assumption.
+Defined.
+
+(** The product of opposite ideals is the opposite of the reversed product. *)
+Definition ideal_product_op {R : Ring} (I J : Ideal R)
+  : (ideal_op R I) ⋅ (ideal_op R J)
+    ↔ ideal_op R (J ⋅ I).
+Proof.
+  rapply ideal_product_type_op.
+Defined.
+
+Definition ideal_product_op_triple {R : Ring} (I J K : Ideal R)
+  : ideal_op R ((K ⋅ J) ⋅ I)
+      ⊆ (ideal_op R I) ⋅ ((ideal_op R J) ⋅ (ideal_op R K)).
+Proof.
+  intros x i.
+  apply (ideal_product_op (R:=rng_op R)).
+  napply (ideal_product_subset_pres_l (R:=R)).
+  1: napply (ideal_product_op (R:=rng_op R)).
+  apply i.
+Defined.
+
+(** The product of ideals is an associative operation. *)
+Definition ideal_product_assoc {R : Ring} (I J K : Ideal R)
+  : I ⋅ (J ⋅ K) ↔ (I ⋅ J) ⋅ K.
+Proof.
+  assert (f : forall (R : Ring) (I J K : Ideal R), I ⋅ (J ⋅ K) ⊆ (I ⋅ J) ⋅ K).
+  - clear R I J K; intros R I J K.
+    napply subgroup_generated_rec.
+    intros _ [r s IHr IHs].
+    revert IHs.
+    rapply (functor_subgroup_generated _ _ (grp_homo_rng_left_mult r)); clear s.
+    intros _ [s t IHs IHt]; cbn.
+    rewrite rng_mult_assoc.
+    by apply ipn_in; [ apply tr, sgt_in, ipn_in | ].
+  - apply pred_subset_antisymm; only 1: apply f.
+    intros x i.
+    apply (ideal_product_op_triple (R:=rng_op R) I J K).
+    napply f.
+    apply ideal_product_op_triple.
+    exact i.
+Defined.
+
+(** Products of ideals are subsets of their intersection. *)
+Definition ideal_product_subset_intersection {R : Ring} (I J : Ideal R)
+  : I ⋅ J ⊆ I ∩ J.
+Proof.
+  apply ideal_intersection_subset.
+  + apply ideal_product_subset_l.
+  + apply ideal_product_subset_r.
+Defined.
+
+(** Sums of ideals are the smallest ideal containing the summands. *)
+Definition ideal_sum_smallest {R : Ring} (I J K : Ideal R)
+  : I ⊆ K -> J ⊆ K -> (I + J) ⊆ K.
+Proof.
+  intros p q.
+  refine (ideal_sum_ind I J (fun x _ => K x) p q _ _).
+  1: apply ideal_in_zero.
+  intros y z s t.
+  rapply ideal_in_plus_negate.
+Defined.
+
+(** Ideals absorb themselves under sum. *)
+Definition ideal_sum_self {R : Ring} (I : Ideal R)
+  : I + I ↔ I.
+Proof.
+  apply pred_subset_antisymm.
+  1: by rapply ideal_sum_smallest.
+  rapply ideal_sum_subset_l.
+Defined.
+
+(** Sums preserve inclusions in the left summand. *)
+Definition ideal_sum_subset_pres_l {R : Ring} (I J K : Ideal R)
+  : I ⊆ J -> (I + K) ⊆ (J + K).
+Proof.
+  intros p.
+  apply ideal_sum_smallest.
+  { transitivity J.
     1: exact p.
-    apply ideal_sum_subset_r.
-  Defined.
-
-  (** Products left distribute over sums *)
-  (** Note that this follows from left adjoints preserving colimits. The product of ideals is a functor whose right adjoint is the quotient ideal. *)
-  Lemma ideal_dist_l (I J K : Ideal R) : I ⋅ (J + K) ↔ I ⋅ J + I ⋅ K.
-  Proof.
-    (** We split into two directions. *)
-    apply ideal_subset_antisymm.
-    (** We deal with the difficult inclusion first. The proof comes down to breaking down the definition and reassembling into the right. *)
-    { intros r p.
-      strip_truncations.
-      induction p as [ r i | | r s p1 IHp1 p2 IHp2].
-      - destruct i as [r s p q].
-        strip_truncations.
-        induction q as [ t k | | t k p1 IHp1 p2 IHp2 ].
-        + apply tr, sgt_in.
-          destruct k as [j | k].
-          * left; by apply tr, sgt_in, ipn_in.
-          * right; by apply tr, sgt_in, ipn_in.
-        + apply tr, sgt_in; left.
-          rewrite rng_mult_zero_r.
-          apply ideal_in_zero.
-        + rewrite rng_dist_l.
-          rewrite rng_mult_negate_r.
-          by apply ideal_in_plus_negate.
-      - apply ideal_in_zero.
-      - by apply ideal_in_plus_negate. }
-    (** This is the easy direction which can use previous lemmas. *)
-    apply ideal_sum_smallest.
-    1,2: apply ideal_product_subset_pres_r.
-    1: apply ideal_sum_subset_l.
-    apply ideal_sum_subset_r.
-  Defined.
-
-  (** Products distribute over sums on the right. *)
-  (** The proof is very similar to the left version *)
-  Lemma ideal_dist_r (I J K : Ideal R) : (I + J) ⋅ K ↔ I ⋅ K + J ⋅ K.
-  Proof.
-    apply ideal_subset_antisymm.
-    { intros r p.
-      strip_truncations.
-      induction p as [ r i | | r s p1 IHp1 p2 IHp2].
-      - destruct i as [r s p q].
-        strip_truncations.
-        induction p as [ t k | | t k p1 IHp1 p2 IHp2 ].
-        + apply tr, sgt_in.
-          destruct k as [j | k].
-          * left; by apply tr, sgt_in, ipn_in.
-          * right; by apply tr, sgt_in, ipn_in.
-        + apply tr, sgt_in; left.
-          rewrite rng_mult_zero_l.
-          apply ideal_in_zero.
-        + rewrite rng_dist_r.
-          rewrite rng_mult_negate_l.
-          by apply ideal_in_plus_negate.
-      - apply ideal_in_zero.
-      - by apply ideal_in_plus_negate. }
-    apply ideal_sum_smallest.
-    1,2: apply ideal_product_subset_pres_l.
-    1: apply ideal_sum_subset_l.
-    apply ideal_sum_subset_r.
-  Defined.
-
-  (** Ideal sums are commutative *)
-  Lemma ideal_sum_comm (I J : Ideal R) : I + J ↔ J + I.
-  Proof.
-    apply ideal_subset_antisymm; apply ideal_sum_smallest.
-    1,3: apply ideal_sum_subset_r.
-    1,2: apply ideal_sum_subset_l.
-  Defined.
-
-  (** Zero ideal is left additive identity. *) 
-  Lemma ideal_sum_zero_l I : ideal_zero R + I ↔ I.
-  Proof.
-    apply ideal_subset_antisymm.
-    1: apply ideal_sum_smallest.
-    1: apply ideal_zero_subset.
-    1: reflexivity.
-    apply ideal_sum_subset_r.
-  Defined.
-
-  (** Zero ideal is right additive identity. *)
-  Lemma ideal_sum_zero_r I : I + ideal_zero R ↔ I.
-  Proof.
-    apply ideal_subset_antisymm.
-    1: apply ideal_sum_smallest.
-    1: reflexivity.
-    1: apply ideal_zero_subset.
-    apply ideal_sum_subset_l.
-  Defined.
-
-  (** Unit ideal is left multiplicative identity. *)
-  Lemma ideal_product_unit_l I : ideal_unit R ⋅ I ↔ I.
-  Proof.
-    apply ideal_subset_antisymm.
-    1: apply ideal_product_subset_r.
-    intros r p.
-    rewrite <- rng_mult_one_l.
-    by apply tr, sgt_in, ipn_in.
-  Defined.
-
-  (** Unit ideal is right multiplicative identity. *)
-  Lemma ideal_product_unit_r I : I ⋅ ideal_unit R ↔ I.
-  Proof.
-    apply ideal_subset_antisymm.
-    1: apply ideal_product_subset_l.
-    intros r p.
-    rewrite <- rng_mult_one_r.
-    by apply tr, sgt_in, ipn_in.
-  Defined.
-
-  (** Intersecting with unit ideal on the left does nothing. *)
-  Lemma ideal_intresection_unit_l I : ideal_unit R ∩ I ↔ I.
-  Proof.
-    apply ideal_subset_antisymm.
-    1: apply ideal_intersection_subset_r.
-    apply ideal_intersection_subset.
-    1: apply ideal_unit_subset.
-    reflexivity.
-  Defined.
-
-  (** Intersecting with unit ideal on right does nothing. *)
-  Lemma ideal_intersection_unit_r I : I ∩ ideal_unit R ↔ I.
-  Proof.
-    apply ideal_subset_antisymm.
-    1: apply ideal_intersection_subset_l.
-    apply ideal_intersection_subset.
-    1: reflexivity.
-    apply ideal_unit_subset.
-  Defined.
-
-  (** Product of intersection and sum is subset of sum of products *)
-  Lemma ideal_product_intersection_sum_subset (I J : Ideal R)
-    : (I ∩ J) ⋅ (I + J) ⊆ (I ⋅ J + J ⋅ I).
-  Proof.
-    etransitivity.
-    1: rapply ideal_dist_l.
-    etransitivity.
-    1: rapply ideal_sum_subset_pres_r.
-    1: rapply ideal_product_subset_pres_l.
-    1: apply ideal_intersection_subset_l.
-    etransitivity.
-    1: rapply ideal_sum_subset_pres_l.
-    1: rapply ideal_product_subset_pres_l.
-    1: apply ideal_intersection_subset_r.
-    rapply ideal_sum_comm.
-  Defined.
-
-  (** Ideals are subsets of their ideal quotients *)
-  Lemma ideal_quotient_subset (I J : Ideal R) : I ⊆ (I :: J).
-  Proof.
-    intros x i; split; apply tr; intros r j; cbn.
-    - by rapply isrightideal.
-    - by rapply isleftideal.
-  Defined.
-
-  (** If J divides I then the ideal quotient of J by I is trivial. *)
-  Lemma ideal_quotient_trivial (I J : Ideal R)
-    : I ⊆ J -> J :: I ↔ ideal_unit R.
-  Proof.
-    intros p.
-    apply ideal_subset_antisymm.
-    1: cbv; trivial.
-    intros r _; split; apply tr; intros x q; cbn.
-    - by apply isleftideal, p. 
-    - rapply isrightideal.
-      by apply p.
-  Defined.
-
-  (** The ideal quotient of I by unit is I. *)
-  Lemma ideal_quotient_unit_bottom (I : Ideal R)
-    : (I :: ideal_unit R) ↔ I.
-  Proof.
-    apply ideal_subset_antisymm.
-    - intros r [p q].
+    apply ideal_sum_subset_l. }
+  apply ideal_sum_subset_r.
+Defined.
+
+(** Sums preserve inclusions in the right summand. *)
+Definition ideal_sum_subset_pres_r {R : Ring} (I J K : Ideal R)
+  : I ⊆ J -> (K + I) ⊆ (K + J).
+Proof.
+  intros p.
+  apply ideal_sum_smallest.
+  1: apply ideal_sum_subset_l.
+  transitivity J.
+  1: exact p.
+  apply ideal_sum_subset_r.
+Defined.
+
+(** Sums preserve inclusions in both summands. *)
+Definition ideal_sum_subset_pres {R : Ring} (I J K L : Ideal R)
+  : I ⊆ J -> K ⊆ L -> (I + K) ⊆ (J + L).
+Proof.
+  intros p q.
+  transitivity (J + K).
+  1: by apply ideal_sum_subset_pres_l.
+  by apply ideal_sum_subset_pres_r.
+Defined.
+
+(** Sums preserve ideal equality in both summands. *)
+Definition ideal_sum_eq {R : Ring} (I J K L : Ideal R)
+  : I ↔ J -> K ↔ L -> (I + K) ↔ (J + L).
+Proof.
+  intros p q.
+  by apply pred_subset_antisymm; apply ideal_sum_subset_pres; apply pred_eq_subset.
+Defined.
+
+(** The sum of two opposite ideals is the opposite of their sum. *)
+Definition ideal_sum_op {R : Ring} (I J : Ideal R)
+  : ideal_op R I + ideal_op R J ↔ ideal_op R (I + J)
+  := reflexive_pred_eq _.
+
+(** Products left distribute over sums. Note that this follows from left adjoints preserving colimits. The product of ideals is a functor whose right adjoint is the quotient ideal. *)
+Definition ideal_dist_l {R : Ring} (I J K : Ideal R)
+  : I ⋅ (J + K) ↔ I ⋅ J + I ⋅ K.
+Proof.
+  (** We split into two directions. *)
+  apply pred_subset_antisymm.
+  (** We deal with the difficult inclusion first. The proof comes down to breaking down the definition and reassembling into the right. *)
+  { intros r p.
+    strip_truncations.
+    induction p as [ r i | | r s p1 IHp1 p2 IHp2].
+    - destruct i as [r s p q].
       strip_truncations.
-      rewrite <- rng_mult_one_r.
-      exact (p ring_one tt).
-    - apply ideal_quotient_subset.
-  Defined.
-
-  (** The ideal quotient of unit by I is unit. *)
-  Lemma ideal_quotient_unit_top (I : Ideal R)
-    : (ideal_unit R :: I) ↔ ideal_unit R.
-  Proof.
-    split.
-    - cbn; trivial.
-    - intros ?; split; apply tr;
-      cbn; split; trivial. 
-  Defined.
-
-  (** The ideal quotient by a sum is an intersection of ideal quotients. *)
-  Lemma ideal_quotient_sum (I J K : Ideal R)
-    : (I :: (J + K)) ↔ (I :: J) ∩ (I :: K).
-  Proof.
-    apply ideal_subset_antisymm.
-    { intros r [p q]; strip_truncations; split; split; apply tr; intros x jk.
-      - by rapply p; rapply ideal_sum_subset_l.
-      - by rapply q; rapply ideal_sum_subset_l.
-      - by rapply p; rapply ideal_sum_subset_r.
-      - by rapply q; rapply ideal_sum_subset_r. }
-    intros r [[p q] [u v]]; strip_truncations; split; apply tr;
-    intros x jk; strip_truncations.
-    - induction jk as [? [] | | ? ? ? ? ? ? ].
-      + by apply p.
-      + by apply u.
-      + apply u, ideal_in_zero.
+      induction q as [ t k | | t k p1 IHp1 p2 IHp2 ].
+      + apply tr, sgt_in.
+        destruct k as [j | k].
+        * left; by apply tr, sgt_in, ipn_in.
+        * right; by apply tr, sgt_in, ipn_in.
+      + apply tr, sgt_in; left.
+        rewrite rng_mult_zero_r.
+        apply ideal_in_zero.
       + rewrite rng_dist_l.
         rewrite rng_mult_negate_r.
         by apply ideal_in_plus_negate.
-    - induction jk as [? [] | | ? ? ? ? ? ? ].
-      + by apply q.
-      + by apply v.
-      + apply v, ideal_in_zero.
-      + change (I ((g - h) * r)). 
-        rewrite rng_dist_r.
-        rewrite rng_mult_negate_l.
-        by apply ideal_in_plus_negate.
-  Defined.
-
-  (** Ideal quotients distribute over intersections. *)
-  Lemma ideal_quotient_intersection (I J K : Ideal R)
-    : (I ∩ J :: K) ↔ (I :: K) ∩ (J :: K).
-  Proof.
-    apply ideal_subset_antisymm.
-    - intros r [p q]; strip_truncations; split; split; apply tr; intros x k.
-      1,3: by apply p.
-      1,2: by apply q.
-    - intros r [[p q] [u v]].
-      strip_truncations; split; apply tr; intros x k; split.
-      + by apply p.
-      + by apply u.
-      + by apply q.
-      + by apply v.
-  Defined.
-
-  (** Annihilators reverse the order of inclusion. *)
-  Lemma ideal_annihilator_subset (I J : Ideal R) : I ⊆ J -> Ann J ⊆ Ann I.
-  Proof.
-    intros p x [q q']; hnf in q, q'; strip_truncations;
-      split; apply tr; intros y i.
-    - by apply q, p.
-    - by apply q', p.
-  Defined.
-
-  (** The annihilator of an ideal is equal to a quotient of zero. *)
-  Lemma ideal_annihilator_zero_quotient (I : Ideal R)
-    : Ann I ↔ ideal_zero R :: I.
-  Proof.
-    intros x; split.
-    - intros [p q]; strip_truncations; split; apply tr; intros y i.
-      + exact (p y i).
-      + exact (q y i).
-    - intros [p q]; strip_truncations; split; apply tr; intros y i.
-      + exact (p y i).
-      + exact (q y i).
-  Defined.
-  
-End IdealLemmas.
+    - apply ideal_in_zero.
+    - by apply ideal_in_plus_negate. }
+  (** This is the easy direction which can use previous lemmas. *)
+  apply ideal_sum_smallest.
+  1,2: apply ideal_product_subset_pres_r.
+  1: apply ideal_sum_subset_l.
+  apply ideal_sum_subset_r.
+Defined.
+
+(** Products distribute over sums on the right. *)
+Definition ideal_dist_r {R : Ring} (I J K : Ideal R)
+  : (I + J) ⋅ K ↔ I ⋅ K + J ⋅ K.
+Proof.
+  change I with (ideal_op _ (ideal_op R I)).
+  change J with (ideal_op _ (ideal_op R J)).
+  change K with (ideal_op _ (ideal_op R K)).
+  etransitivity.
+  2: rapply ideal_sum_eq; symmetry; apply (ideal_product_op (R:=rng_op R)).
+  etransitivity.
+  2: apply (ideal_dist_l (R:=rng_op R)).
+  etransitivity.
+  2: apply (ideal_product_op (R:=rng_op R)).
+  reflexivity.
+Defined.
+
+(** Ideal sums are commutative *)
+Definition ideal_sum_comm {R : Ring} (I J : Ideal R) : I + J ↔ J + I.
+Proof.
+  apply pred_subset_antisymm; apply ideal_sum_smallest.
+  1,3: apply ideal_sum_subset_r.
+  1,2: apply ideal_sum_subset_l.
+Defined.
+
+(** Zero ideal is left additive identity. *) 
+Definition ideal_sum_zero_l {R : Ring} I : ideal_zero R + I ↔ I.
+Proof.
+  apply pred_subset_antisymm.
+  1: apply ideal_sum_smallest.
+  1: apply ideal_zero_subset.
+  1: reflexivity.
+  apply ideal_sum_subset_r.
+Defined.
+
+(** Zero ideal is right additive identity. *)
+Definition ideal_sum_zero_r {R : Ring} I : I + ideal_zero R ↔ I.
+Proof.
+  apply pred_subset_antisymm.
+  1: apply ideal_sum_smallest.
+  1: reflexivity.
+  1: apply ideal_zero_subset.
+  apply ideal_sum_subset_l.
+Defined.
+
+(** Unit ideal is left multiplicative identity. *)
+Definition ideal_product_unit_l {R : Ring} I : ideal_unit R ⋅ I ↔ I.
+Proof.
+  apply pred_subset_antisymm.
+  1: apply ideal_product_subset_r.
+  intros r p.
+  rewrite <- rng_mult_one_l.
+  by apply tr, sgt_in, ipn_in.
+Defined.
+
+(** Unit ideal is right multiplicative identity. *)
+Definition ideal_product_unit_r {R : Ring} I : I ⋅ ideal_unit R ↔ I.
+Proof.
+  apply pred_subset_antisymm.
+  1: apply ideal_product_subset_l.
+  intros r p.
+  rewrite <- rng_mult_one_r.
+  by apply tr, sgt_in, ipn_in.
+Defined.
+
+(** Intersecting with unit ideal on the left does nothing. *)
+Definition ideal_intresection_unit_l {R : Ring} I : ideal_unit R ∩ I ↔ I.
+Proof.
+  apply pred_subset_antisymm.
+  1: apply ideal_intersection_subset_r.
+  apply ideal_intersection_subset.
+  1: apply ideal_unit_subset.
+  reflexivity.
+Defined.
+
+(** Intersecting with unit ideal on right does nothing. *)
+Definition ideal_intersection_unit_r {R : Ring} I : I ∩ ideal_unit R ↔ I.
+Proof.
+  apply pred_subset_antisymm.
+  1: apply ideal_intersection_subset_l.
+  apply ideal_intersection_subset.
+  1: reflexivity.
+  apply ideal_unit_subset.
+Defined.
+
+(** Product of intersection and sum is subset of sum of products *)
+Definition ideal_product_intersection_sum_subset {R : Ring} (I J : Ideal R)
+  : (I ∩ J) ⋅ (I + J) ⊆ (I ⋅ J + J ⋅ I).
+Proof.
+  etransitivity.
+  1: rapply ideal_dist_l.
+  etransitivity.
+  1: rapply ideal_sum_subset_pres_r.
+  1: rapply ideal_product_subset_pres_l.
+  1: apply ideal_intersection_subset_l.
+  etransitivity.
+  1: rapply ideal_sum_subset_pres_l.
+  1: rapply ideal_product_subset_pres_l.
+  1: apply ideal_intersection_subset_r.
+  rapply ideal_sum_comm.
+Defined.
+
+(** Ideals are subsets of their ideal quotients *)
+Definition ideal_quotient_subset {R : Ring} (I J : Ideal R) : I ⊆ (I :: J).
+Proof.
+  intros x i; split; apply tr; intros r j; cbn.
+  - by rapply isrightideal.
+  - by rapply isleftideal.
+Defined.
+
+(** If J divides I then the ideal quotient of J by I is trivial. *)
+Definition ideal_quotient_trivial {R : Ring} (I J : Ideal R)
+  : I ⊆ J -> J :: I ↔ ideal_unit R.
+Proof.
+  intros p.
+  apply pred_subset_antisymm.
+  1: cbv; trivial.
+  intros r _; split; apply tr; intros x q; cbn.
+  - by apply isleftideal, p. 
+  - rapply isrightideal.
+    by apply p.
+Defined.
+
+(** The ideal quotient of I by unit is I. *)
+Definition ideal_quotient_unit_bottom {R : Ring} (I : Ideal R)
+  : (I :: ideal_unit R) ↔ I.
+Proof.
+  apply pred_subset_antisymm.
+  - intros r [p q].
+    strip_truncations.
+    rewrite <- rng_mult_one_r.
+    exact (p ring_one tt).
+  - apply ideal_quotient_subset.
+Defined.
+
+(** The ideal quotient of unit by I is unit. *)
+Definition ideal_quotient_unit_top {R : Ring} (I : Ideal R)
+  : (ideal_unit R :: I) ↔ ideal_unit R.
+Proof.
+  split.
+  - cbn; trivial.
+  - intros ?; split; apply tr;
+    cbn; split; trivial. 
+Defined.
+
+(** The ideal quotient by a sum is an intersection of ideal quotients. *)
+Definition ideal_quotient_sum {R : Ring} (I J K : Ideal R)
+  : (I :: (J + K)) ↔ (I :: J) ∩ (I :: K).
+Proof.
+  apply pred_subset_antisymm.
+  { intros r [p q]; strip_truncations; split; split; apply tr; intros x jk.
+    - by rapply p; rapply ideal_sum_subset_l.
+    - by rapply q; rapply ideal_sum_subset_l.
+    - by rapply p; rapply ideal_sum_subset_r.
+    - by rapply q; rapply ideal_sum_subset_r. }
+  intros r [[p q] [u v]]; strip_truncations; split; apply tr;
+  intros x jk; strip_truncations.
+  - induction jk as [? [] | | ? ? ? ? ? ? ].
+    + by apply p.
+    + by apply u.
+    + apply u, ideal_in_zero.
+    + rewrite rng_dist_l.
+      rewrite rng_mult_negate_r.
+      by apply ideal_in_plus_negate.
+  - induction jk as [? [] | | ? ? ? ? ? ? ].
+    + by apply q.
+    + by apply v.
+    + apply v, ideal_in_zero.
+    + change (I ((g - h) * r)). 
+      rewrite rng_dist_r.
+      rewrite rng_mult_negate_l.
+      by apply ideal_in_plus_negate.
+Defined.
+
+(** Ideal quotients distribute over intersections. *)
+Definition ideal_quotient_intersection {R : Ring} (I J K : Ideal R)
+  : (I ∩ J :: K) ↔ (I :: K) ∩ (J :: K).
+Proof.
+  apply pred_subset_antisymm.
+  - intros r [p q]; strip_truncations; split; split; apply tr; intros x k.
+    1,3: by apply p.
+    1,2: by apply q.
+  - intros r [[p q] [u v]].
+    strip_truncations; split; apply tr; intros x k; split.
+    + by apply p.
+    + by apply u.
+    + by apply q.
+    + by apply v.
+Defined.
+
+(** Annihilators reverse the order of inclusion. *)
+Definition ideal_annihilator_subset {R : Ring} (I J : Ideal R)
+  : I ⊆ J -> Ann J ⊆ Ann I.
+Proof.
+  intros p x [q q']; hnf in q, q'; strip_truncations;
+    split; apply tr; intros y i.
+  - by apply q, p.
+  - by apply q', p.
+Defined.
+
+(** The annihilator of an ideal is equal to a quotient of zero. *)
+Definition ideal_annihilator_zero_quotient {R : Ring} (I : Ideal R)
+  : Ann I ↔ ideal_zero R :: I.
+Proof.
+  intros x; split.
+  - intros [p q]; strip_truncations; split; apply tr; intros y i.
+    + exact (p y i).
+    + exact (q y i).
+  - intros [p q]; strip_truncations; split; apply tr; intros y i.
+    + exact (p y i).
+    + exact (q y i).
+Defined.
 
 (** ** Preimage of ideals under ring homomorphisms *)
 
diff --git a/theories/Basics.v b/theories/Basics.v
index 09f1c86655..8231e0d3b5 100644
--- a/theories/Basics.v
+++ b/theories/Basics.v
@@ -9,6 +9,7 @@ Require Export Basics.Notations.
 Require Export Basics.Tactics.
 Require Export Basics.Classes.
 Require Export Basics.Iff.
+Require Export Basics.Predicate.
 
 Require Export Basics.Nat.
 Require Export Basics.Numeral.
diff --git a/theories/Basics/Classes.v b/theories/Basics/Classes.v
index a4d120e7e6..56d00c1dba 100644
--- a/theories/Basics/Classes.v
+++ b/theories/Basics/Classes.v
@@ -2,6 +2,34 @@ Require Import Basics.Overture Basics.Tactics.
 
 (** * Classes *)
 
+(** ** Pointwise Lemmas *)
+
+Section Pointwise.
+
+  Context {A : Type} {B : A -> Type} (R : forall a, Relation (B a)).
+
+  Definition reflexive_pointwise `{!forall a, Reflexive (R a)}
+    : Reflexive (fun (P Q : forall x, B x) => forall x, R x (P x) (Q x)).
+  Proof.
+    intros P x; reflexivity.
+  Defined.
+
+  Definition transitive_pointwise `{!forall a, Transitive (R a)}
+    : Transitive (fun (P Q : forall x, B x) => forall x, R x (P x) (Q x)).
+  Proof.
+    intros P Q S x y a.
+    by transitivity (Q a).
+  Defined.
+
+  Definition symmetric_pointwise `{!forall a, Symmetric (R a)}
+    : Symmetric (fun (P Q : forall x, B x) => forall x, R x (P x) (Q x)).
+  Proof.
+    intros P Q x a.
+    by symmetry.
+  Defined.
+
+End Pointwise.
+
 (** ** Injective Functions *)
 
 Class IsInjective {A B : Type} (f : A -> B)
diff --git a/theories/Basics/Predicate.v b/theories/Basics/Predicate.v
new file mode 100644
index 0000000000..57fa468b8e
--- /dev/null
+++ b/theories/Basics/Predicate.v
@@ -0,0 +1,79 @@
+Require Import Basics.Overture Basics.Tactics Basics.Iff Basics.Classes.
+
+Set Universe Minimization ToSet.
+
+(** * Predicates on types *)
+
+(** We use the words "subset" and "predicate" interchangably. There is no actual set requirement however. *)
+
+(** ** Predicate equality *)
+
+Definition pred_eq {A : Type} (P Q : A -> Type) := forall x, P x <-> Q x.
+
+Instance reflexive_pred_eq {A : Type} : Reflexive (@pred_eq A)
+  := reflexive_pointwise (fun _ => _).
+
+Instance symmetric_pred_eq {A : Type} : Symmetric (@pred_eq A)
+  := symmetric_pointwise (fun _ => _).
+
+Instance transitive_pred_eq {A : Type} : Transitive (@pred_eq A)
+  := transitive_pointwise (fun _ => _).
+
+(** ** Subsets of a predicate *)
+
+Definition pred_subset {A : Type} (P Q : A -> Type) := (forall x, P x -> Q x).
+
+(** TODO: move *)
+Instance reflexive_fun : Reflexive (fun A B => A -> B)
+  := fun _ => idmap.
+
+(** TODO: move *)
+Instance transitive_fun : Transitive (fun A B => A -> B)
+  := fun _ _ _ f g => g o f.
+
+(** The subset relation is reflexive. *)
+Instance reflexive_pred_subset {A : Type} : Reflexive (@pred_subset A)
+  := reflexive_pointwise (B:=fun x => Type) (fun _ A B => A -> B).
+
+(** The subset relation is transitive. *)
+Instance transitive_pred_subset {A : Type} : Transitive (@pred_subset A)
+ := transitive_pointwise (B:=fun x => Type) (fun _ A B => A -> B).
+
+Coercion pred_eq_subset {A : Type} (P Q : A -> Type)
+  : pred_eq P Q -> pred_subset P Q
+  := fun p x => fst (p x).
+
+Definition pred_eq_subset' {A : Type} (P Q : A -> Type)
+  : pred_eq P Q -> pred_subset Q P
+  := fun p x => snd (p x).
+
+Definition pred_subset_precomp {A B : Type} {P Q : B -> Type} (f : A -> B)
+  : pred_subset P Q -> pred_subset (P o f) (Q o f).
+Proof.
+  intros p x; apply p.
+Defined.
+
+Definition pred_subset_moveL_equiv {A B : Type} {P : B -> Type} {Q : A -> Type}
+  (f : A <~> B)
+  : pred_subset (P o f) Q -> pred_subset P (Q o f^-1).
+Proof.
+  intros r b p.
+  apply r.
+  nrefine (_^ # p).
+  apply eisretr.
+Defined.
+
+Definition pred_subset_moveR_equiv {A B : Type} {P : B -> Type} {Q : A -> Type}
+  (f : A <~> B)
+  : pred_subset P (Q o f^-1) -> pred_subset (P o f) Q.
+Proof.
+  intros r a p.
+  exact (eissect _ _ # r _ p).
+Defined.
+
+(** The subset relation is antisymmetric. Note that this isn't [Antisymmetry] as defined in [Basics.Classes] since we get a [pred_eq] rather than a path. Under being a hprop and univalnce, we would get a path. *)
+Definition pred_subset_antisymm {A : Type} {P Q : A -> Type}
+  : pred_subset P Q -> pred_subset Q P -> pred_eq P Q.
+Proof.
+  intros p q x; specialize (p x); specialize (q x); by split.
+Defined.