diff --git a/theories/Algebra/AbGroups/AbelianGroup.v b/theories/Algebra/AbGroups/AbelianGroup.v
index 5cd6a5d22ec..0e84f177736 100644
--- a/theories/Algebra/AbGroups/AbelianGroup.v
+++ b/theories/Algebra/AbGroups/AbelianGroup.v
@@ -29,6 +29,28 @@ Proof.
   split; exact _.
 Defined.
 
+(** Easier way to build abelian groups without redundant information. *)
+Definition Build_AbGroup' (G : Type)
+  `{Zero G, Negate G, Plus G, IsHSet G}
+  (comm : Commutative (A:=G) (+))
+  (assoc : Associative (A:=G) (+))
+  (unit_l : LeftIdentity (A:=G) (+) 0)
+  (inv_l : LeftInverse (A:=G) (+) (-) 0)
+  : AbGroup.
+Proof.
+  snrapply Build_AbGroup.
+  - (* TODO: introduce smart constructor for [Build_Group] *)
+    rapply (Build_Group G).
+    repeat split; only 1-3, 5: exact _.
+    + intros x.
+      lhs nrapply comm.
+      exact (unit_l x).
+    + intros x.
+      lhs nrapply comm.
+      exact (inv_l x).
+  - exact comm.
+Defined.
+
 Definition issig_abgroup : _ <~> AbGroup := ltac:(issig).
 
 Global Instance zero_abgroup (A : AbGroup) : Zero A := group_unit.
@@ -91,11 +113,7 @@ Global Instance isabgroup_quotient (G : AbGroup) (H : Subgroup G)
 Proof.
   nrapply Build_IsAbGroup.
   1: exact _.
-  intro x.
-  srapply Quotient_ind_hprop.
-  intro y; revert x.
-  srapply Quotient_ind_hprop.
-  intro x.
+  srapply Quotient_ind2_hprop; intros x y.
   apply (ap (class_of _)).
   apply commutativity.
 Defined.
diff --git a/theories/Algebra/AbGroups/Z.v b/theories/Algebra/AbGroups/Z.v
index c8a31d9eec2..2c9b32a525f 100644
--- a/theories/Algebra/AbGroups/Z.v
+++ b/theories/Algebra/AbGroups/Z.v
@@ -12,14 +12,16 @@ Local Open Scope int_scope.
 
 Definition abgroup_Z@{} : AbGroup@{Set}.
 Proof.
-  snrapply Build_AbGroup.
-  - refine (Build_Group Int int_add 0 int_neg _); repeat split.
-    + exact _.
-    + exact int_add_assoc.
-    + exact int_add_0_r.
-    + exact int_add_neg_l.
-    + exact int_add_neg_r.
+  snrapply Build_AbGroup'.
+  - exact Int.
+  - exact 0.
+  - exact int_neg.
+  - exact int_add.
+  - exact _.
   - exact int_add_comm.
+  - exact int_add_assoc.
+  - exact int_add_0_l.
+  - exact int_add_neg_l.
 Defined.
 
 (** For every group [G] and element [g : G], the map sending an integer to that power of [g] is a homomorphism.  See [ab_mul] for the homomorphism [G -> G] when [G] is abelian. *)
diff --git a/theories/Algebra/AbSES/Core.v b/theories/Algebra/AbSES/Core.v
index 4d0cfa3432a..6d76b4e707e 100644
--- a/theories/Algebra/AbSES/Core.v
+++ b/theories/Algebra/AbSES/Core.v
@@ -737,8 +737,7 @@ Proof.
   - apply isequiv_surj_emb.
     1: rapply cancelR_conn_map.
     apply isembedding_isinj_hset.
-    srapply Quotient_ind_hprop; intro x.
-    srapply Quotient_ind_hprop; intro y.
+    srapply Quotient_ind2_hprop; intros x y.
     intro p.
     apply qglue; cbn.
     refine (isexact_preimage (Tr (-1)) _ _ (-x + y) _).
diff --git a/theories/Algebra/Groups/QuotientGroup.v b/theories/Algebra/Groups/QuotientGroup.v
index 9acacb0232d..91c0c3396f1 100644
--- a/theories/Algebra/Groups/QuotientGroup.v
+++ b/theories/Algebra/Groups/QuotientGroup.v
@@ -27,23 +27,12 @@ Section GroupCongruenceQuotient.
 
   Global Instance congquot_sgop : SgOp CongruenceQuotient.
   Proof.
-    intros x.
-    srapply Quotient_rec.
-    { intro y; revert x.
-      srapply Quotient_rec.
-      { intros x.
-        apply class_of.
-        exact (x * y). }
-      intros a b r.
-      cbn.
+    srapply Quotient_rec2.
+    - intros x y.
+      exact (class_of _ (x * y)).
+    - intros x x' p y y' q.
       apply qglue.
-      by apply iscong. }
-    intros a b r.
-    revert x.
-    srapply Quotient_ind_hprop.
-    intro x.
-    apply qglue.
-    by apply iscong.
+      by apply iscong.
   Defined.
 
   Global Instance congquot_mon_unit : MonUnit CongruenceQuotient.
@@ -72,10 +61,7 @@ Section GroupCongruenceQuotient.
 
   Global Instance congquot_sgop_associative : Associative congquot_sgop.
   Proof.
-    intros x y.
-    srapply Quotient_ind_hprop; intro a; revert y.
-    srapply Quotient_ind_hprop; intro b; revert x.
-    srapply Quotient_ind_hprop; intro c.
+    srapply Quotient_ind3_hprop; intros x y z.
     simpl; by rewrite associativity.
   Qed.
 
diff --git a/theories/Algebra/Rings/CRing.v b/theories/Algebra/Rings/CRing.v
index fd803e35f42..1259284c0fb 100644
--- a/theories/Algebra/Rings/CRing.v
+++ b/theories/Algebra/Rings/CRing.v
@@ -2,7 +2,7 @@ Require Import WildCat.
 (* Some of the material in abstract_algebra and canonical names could be selectively exported to the user, as is done in Groups/Group.v. *)
 Require Import Classes.interfaces.abstract_algebra.
 Require Import Algebra.AbGroups.
-Require Export Algebra.Rings.Ring Algebra.Rings.Ideal.
+Require Export Algebra.Rings.Ring Algebra.Rings.Ideal Algebra.Rings.QuotientRing.
 
 (** * Commutative Rings *)
 
@@ -23,17 +23,21 @@ Global Instance cring_plus {R : CRing} : Plus R := plus_abgroup R.
 Global Instance cring_zero {R : CRing} : Zero R := zero_abgroup R.
 Global Instance cring_negate {R : CRing} : Negate R := negate_abgroup R.
 
-Definition Build_CRing' (R : AbGroup)
-  `(!One R, !Mult R, !Commutative (.*.), !LeftDistribute (.*.) (+), @IsMonoid R (.*.) 1)
+Definition Build_CRing' (R : AbGroup) `(!One R, !Mult R)
+  (comm : Commutative (.*.)) (assoc : Associative (.*.))
+  (dist_l : LeftDistribute (.*.) (+)) (unit_l : LeftIdentity (.*.) 1)
   : CRing.
 Proof.
   snrapply Build_CRing.
-  - snrapply (Build_Ring R).
-    1-3,5: exact _.
-    intros x y z.
-    lhs rapply commutativity.
-    lhs rapply simple_distribute_l.
-    f_ap.
+  - rapply (Build_Ring R); only 1: exact _.
+    2: repeat split; only 1-3: exact _.
+    + intros x y z.
+      lhs nrapply comm.
+      lhs rapply dist_l.
+      f_ap.
+    + intros x.
+      lhs rapply comm.
+      apply unit_l.
   - exact _.
 Defined.
 
@@ -56,6 +60,38 @@ Proof.
   f_ap.
 Defined.
 
+Definition rng_mult_permute_2_3 {R : CRing} (x y z : R)
+  : x * y * z = x * z * y.
+Proof.
+  lhs_V nrapply rng_mult_assoc.
+  rhs_V nrapply rng_mult_assoc.
+  apply ap, rng_mult_comm.
+Defined.
+
+Definition rng_mult_move_left_assoc {R : CRing} (x y z : R)
+  : x * y * z = y * x * z.
+Proof.
+  f_ap; apply rng_mult_comm.
+Defined.
+
+Definition rng_mult_move_right_assoc {R : CRing} (x y z : R)
+  : x * (y * z) = y * (x * z).
+Proof.
+  refine (rng_mult_assoc _ _ _ @ _ @ (rng_mult_assoc _ _ _)^).
+  apply rng_mult_move_left_assoc.
+Defined.
+
+Definition isinvertible_cring (R : CRing) (x : R)
+  (inv : R) (inv_l : inv * x = 1)
+  : IsInvertible R x.
+Proof.
+  snrapply Build_IsInvertible.
+  - exact inv.
+  - exact inv_l.
+  - lhs nrapply rng_mult_comm.
+    exact inv_l.
+Defined.
+
 (** ** Ideals in commutative rings *)
   
 Section IdealCRing.
@@ -223,3 +259,23 @@ Global Instance is01cat_CRing : Is01Cat CRing := is01cat_induced cring_ring.
 Global Instance is2graph_CRing : Is2Graph CRing := is2graph_induced cring_ring.
 Global Instance is1cat_CRing : Is1Cat CRing := is1cat_induced cring_ring.
 Global Instance hasequiv_CRing : HasEquivs CRing := hasequivs_induced cring_ring.
+
+(** ** Quotient rings *)
+
+Global Instance commutative_quotientring_mult (R : CRing) (I : Ideal R)
+  : Commutative (A:=QuotientRing R I) (.*.).
+Proof.
+  intros x; srapply QuotientRing_ind_hprop; intros y; revert x.
+  srapply QuotientRing_ind_hprop; intros x; hnf.
+  lhs_V nrapply rng_homo_mult.
+  rhs_V nrapply rng_homo_mult.
+  snrapply ap.
+  apply commutativity.
+Defined.
+
+Definition cring_quotient (R : CRing) (I : Ideal R) : CRing
+  := Build_CRing (QuotientRing R I) _.
+
+Definition cring_quotient_map {R : CRing} (I : Ideal R)
+  : R $-> cring_quotient R I
+  := rng_quotient_map I.
diff --git a/theories/Algebra/Rings/Localization.v b/theories/Algebra/Rings/Localization.v
new file mode 100644
index 00000000000..2e5197ca3a7
--- /dev/null
+++ b/theories/Algebra/Rings/Localization.v
@@ -0,0 +1,545 @@
+Require Import Basics.Overture Basics.Trunc Basics.Tactics Colimits.Quotient
+  abstract_algebra Rings.CRing Truncations.Core Nat.Core
+  Rings.QuotientRing WildCat.Core WildCat.Equiv.
+
+Local Open Scope mc_scope.
+
+(** * Localization of commutative rings *)
+
+(** Localization is a way to make elements in a commutative ring invertible by adding inverses, in the most minimal way possible. It generalizes the familiar operation of a field of fractions. *)
+
+(** ** Multiplicative subsets *)
+
+(** A multiplicative subset is formally a submonoid of the multiplicative monoid of a ring. Essentially it is a subset closed under finite products. *)
+
+(** *** Definition *)
+
+(** Multiplicative subsets of a ring [R] consist of: *)
+Class IsMultiplicativeSubset {R : CRing} (S : R -> Type) : Type := {
+  (** Contains one *)
+  mss_one : S 1 ;
+  (** Closed under multiplication *)
+  mss_mult : forall x y, S x -> S y -> S (x * y) ;
+}.
+
+Arguments mss_one {R _ _}.
+Arguments mss_mult {R _ _ _ _}.
+
+(** *** Examples *)
+
+(** The multiplicative subset of powers of a ring element. *)
+Global Instance ismultiplicative_powers (R : CRing) (x : R)
+  : IsMultiplicativeSubset (fun r => exists n, rng_power x n = r).
+Proof.
+  srapply Build_IsMultiplicativeSubset; cbn beta.
+  1: by exists 0%nat.
+  intros a b np mq.
+  destruct np as [n p], mq as [m q].
+  exists (n + m)%nat.
+  lhs_V nrapply rng_power_mult_law.
+  f_ap.
+Defined.
+
+(** Invertible elements of a ring form a multiplicative subset. *)
+Global Instance ismultiplicative_isinvertible (R : CRing)
+  : IsMultiplicativeSubset (@IsInvertible R) := {}.
+
+(** TODO: Property of being a localization. *)
+
+(** ** Construction of localization *)
+
+Section Localization.
+
+  (** We now construct the localization of a ring at a multiplicative subset as the following HIT:
+
+  <<<
+  HIT (Quotient fraction_eq) (R : CRing) (S : R -> Type)
+    `{IsMultiplicativeSubset R} :=
+  | loc_frac (n d : R) (p : S d) : Localization R S
+  | loc_frac_eq (n1 d1 n2 d2 : R) (p1 : S d1) (p2 : S d2)
+      (x : R) (q : S x) (r : x * (d2 * n1 - n2 * d1) = 0)
+      : loc_frac n1 d1 p1 = loc_frac n2 d2 p2
+  .
+  >>>
+  along with the condition that this HIT be a set.
+
+  We will implement this HIT by writing it as a set quotient. From now onwards, [loc_frac] will be implemented as [class_of fraction_eq] and [loc_frac_eq] will be implemented as [qglue]. *)
+
+  Context (R : CRing) (S : R -> Type) `{!IsMultiplicativeSubset S}.
+
+  (** *** Construction of underlying Localization type *)
+
+  (** The base type will be the type of fractions with respect to a multiplicative subset. This consists of pairs of elements of a ring [R] where the [denominator] is in the multiplicative subset [S]. *)
+  Record Fraction := {
+    numerator : R ;
+    denominator : R ;
+    in_mult_subset_denominator : S denominator ;
+  }.
+
+  (** We consider two fractions to be equal if we can rearrange the fractions as products and ask for equality upto some scaling factor from the multiplicative subset [S]. *)
+  Definition fraction_eq : Relation Fraction.
+  Proof.
+    intros [n1 d1 ?] [n2 d2 ?].
+    refine (exists (x : R), S x /\ _).
+    exact (x * n1 * d2 = x * n2 * d1).
+  Defined.
+
+  (** It is convenient to produce elements of this relation specalized to when the scaling factor is [1]. *)
+  Definition fraction_eq_simple f1 f2
+    (p : numerator f1 * denominator f2 = numerator f2 * denominator f1)
+    : fraction_eq f1 f2.
+  Proof.
+    exists 1.
+    refine (mss_one, _).
+    lhs_V nrapply rng_mult_assoc.
+    rhs_V nrapply rng_mult_assoc.
+    exact (ap (1 *.) p).
+  Defined.
+
+  (** Fraction equality is a reflexive relation. *)
+  Definition fraction_eq_refl f1 : fraction_eq f1 f1.
+  Proof.
+    apply fraction_eq_simple.
+    reflexivity.
+  Defined.
+
+  (** Elements of [R] can be considered fractions. *)
+  Definition frac_in : R -> Fraction
+    := fun r => Build_Fraction r 1 mss_one.
+
+  (** Now that we have defined the HIT as above, we can define the ring structure. *)
+
+  (** *** Addition operation *)
+
+  (** Fraction addition is the usual addition of fractions. *)
+  Definition frac_add : Fraction -> Fraction -> Fraction :=
+    fun '(Build_Fraction n1 d1 p1) '(Build_Fraction n2 d2 p2)
+      => Build_Fraction (n1 * d2 + n2 * d1) (d1 * d2) (mss_mult p1 p2).
+
+  (** Fraction addition is well-defined upto equality of fractions. *)
+
+  (** It is easier to prove well-definedness as a function of both arguments at once. *)
+  Definition frac_add_wd (f1 f1' f2 f2' : Fraction)
+    (p : fraction_eq f1 f1') (q : fraction_eq f2 f2')
+    : fraction_eq (frac_add f1 f2) (frac_add f1' f2').
+  Proof.
+    destruct f1 as [a s ss], f1' as [a' s' ss'],
+      f2 as [b t st], f2' as [b' t' st'],
+      p as [x [sx p]], q as [y [sy q]].
+    refine (x * y ; (mss_mult sx sy, _)).
+    simpl.
+    rewrite 2 rng_dist_l, 2 rng_dist_r.
+    snrapply (ap011 (+)). 
+    - rewrite 4 rng_mult_assoc.
+      rewrite 8 (rng_mult_permute_2_3 _ y).
+      apply (ap (.* y)).
+      rewrite 2 (rng_mult_permute_2_3 _ t).
+      apply (ap (.* t)).
+      rewrite (rng_mult_permute_2_3 _ t').
+      f_ap.
+    - do 2 lhs_V nrapply rng_mult_assoc.
+      do 2 rhs_V nrapply rng_mult_assoc.
+      f_ap.
+      rewrite 6 rng_mult_assoc.
+      rewrite 2 (rng_mult_permute_2_3 _ _ t').
+      rewrite 2 (rng_mult_permute_2_3 _ _ t).
+      lhs_V nrapply rng_mult_assoc.
+      rhs_V nrapply rng_mult_assoc.
+      f_ap; apply rng_mult_comm.
+  Defined.
+
+  Definition frac_add_wd_l (f1 f1' f2 : Fraction) (p : fraction_eq f1 f1')
+    : fraction_eq (frac_add f1 f2) (frac_add f1' f2).
+  Proof.
+    pose (fraction_eq_refl f2).
+    by apply frac_add_wd.
+  Defined.
+
+  Definition frac_add_wd_r (f1 f2 f2' : Fraction) (p : fraction_eq f2 f2')
+    : fraction_eq (frac_add f1 f2) (frac_add f1 f2').
+  Proof.
+    pose (fraction_eq_refl f1).
+    by apply frac_add_wd.
+  Defined.
+
+  (** The addition operation on the localization is induced from the addition operation for fractions. *)
+  Instance plus_rng_localization : Plus (Quotient fraction_eq).
+  Proof.
+    srapply Quotient_rec2.
+    - rapply fraction_eq_refl.
+    - cbn.
+      intros f1 f2.
+      exact (class_of _ (frac_add f1 f2)).
+    - cbn beta.
+      intros f1 f1' p f2 f2' q.
+      by apply qglue, frac_add_wd.
+  Defined.
+
+  (** *** Multiplication operation *)
+
+  Definition frac_mult : Fraction -> Fraction -> Fraction :=
+    fun '(Build_Fraction n1 d1 p1) '(Build_Fraction n2 d2 p2)
+      => Build_Fraction (n1 * n2) (d1 * d2) (mss_mult p1 p2).
+
+  Definition frac_mult_wd_l f1 f1' f2 (p : fraction_eq f1 f1')
+    : fraction_eq (frac_mult f1 f2) (frac_mult f1' f2).
+  Proof.
+    destruct p as [x [s p]].
+    refine (x; (s, _)); simpl.
+    rewrite 4 rng_mult_assoc.
+    rewrite (rng_mult_permute_2_3 _ _ (denominator f1')).
+    rewrite (rng_mult_permute_2_3 _ _ (denominator f1)).
+    lhs_V nrapply rng_mult_assoc.
+    rhs_V nrapply rng_mult_assoc.
+    f_ap.
+  Defined.
+
+  Definition frac_mult_wd_r f1 f2 f2' (p : fraction_eq f2 f2')
+    : fraction_eq (frac_mult f1 f2) (frac_mult f1 f2').
+  Proof.
+    destruct p as [x [s p]].
+    refine (x; (s, _)); simpl.
+    rewrite 4 rng_mult_assoc.
+    rewrite (rng_mult_permute_2_3 _ _ (numerator f2)).
+    rewrite 2 (rng_mult_permute_2_3 _ _ (denominator f2')).
+    rewrite (rng_mult_permute_2_3 _ _ (numerator f2')).
+    rewrite 2 (rng_mult_permute_2_3 _ _ (denominator f2)).
+    lhs_V nrapply rng_mult_assoc.
+    rhs_V nrapply rng_mult_assoc.
+    f_ap.
+  Defined.
+
+  Instance mult_rng_localization: Mult (Quotient fraction_eq).
+  Proof.
+    srapply Quotient_rec2.
+    - rapply fraction_eq_refl.
+    - cbn.
+      intros f1 f2.
+      exact (class_of _ (frac_mult f1 f2)).
+    - cbn beta.
+      intros f1 f1' p f2 f2' q.
+      transitivity (class_of fraction_eq (frac_mult f1' f2)).
+      + by apply qglue, frac_mult_wd_l.
+      + by apply qglue, frac_mult_wd_r.
+  Defined.
+
+  (** *** Zero element *)
+
+  Instance zero_rng_localization : Zero (Quotient fraction_eq)
+    := class_of _ (Build_Fraction 0 1 mss_one).
+
+  (** *** One element *)
+
+  Instance one_rng_localization : One (Quotient fraction_eq)
+    := class_of _(Build_Fraction 1 1 mss_one).
+
+  (** *** Negation operation *)
+
+  Definition frac_negate : Fraction -> Fraction
+    :=  fun '(Build_Fraction n d p) => Build_Fraction (- n) d p.
+
+  Definition frac_negate_wd f1 f2 (p : fraction_eq f1 f2)
+    : fraction_eq (frac_negate f1) (frac_negate f2).
+  Proof.
+    destruct p as [x [s p]].
+    refine (x; (s,_)); simpl.
+    rewrite 2 rng_mult_negate_r, 2 rng_mult_negate_l.
+    f_ap.
+  Defined.
+
+  Instance negate_rng_localization : Negate (Quotient fraction_eq).
+  Proof.
+    srapply Quotient_rec.
+    - intros f.
+      apply class_of.
+      exact (frac_negate f).
+    - intros f1 f2 p.
+      by apply qglue, frac_negate_wd.
+  Defined.
+
+  (** *** Ring laws *)
+  
+  (** Commutativity of addition *)
+  Instance commutative_plus_rng_localization
+    : Commutative plus_rng_localization.
+  Proof.
+    srapply Quotient_ind2_hprop; intros x y.
+    apply qglue, fraction_eq_simple; simpl.
+    rewrite (rng_mult_comm (denominator y) (denominator x)).
+    f_ap; apply rng_plus_comm.
+  Defined.
+
+  (** Left additive identity *)
+  Instance leftidentity_plus_rng_localization
+    : LeftIdentity plus_rng_localization zero_rng_localization.
+  Proof.
+    srapply Quotient_ind_hprop; intros f.
+    apply qglue, fraction_eq_simple; simpl.
+    f_ap.
+    - rewrite rng_mult_zero_l.
+      rewrite rng_plus_zero_l.
+      apply rng_mult_one_r.
+    - symmetry.
+      apply rng_mult_one_l.
+  Defined.
+
+  Instance leftinverse_plus_rng_localization
+    : LeftInverse plus_rng_localization negate_rng_localization zero_rng_localization.
+  Proof.
+    srapply Quotient_ind_hprop; intros f.
+    apply qglue, fraction_eq_simple; simpl.
+    refine (rng_mult_one_r _ @ _).
+    refine (_ @ (rng_mult_zero_l _)^).
+    rewrite rng_mult_negate_l.
+    apply rng_plus_negate_l.
+  Defined.
+
+  Instance associative_plus_rng_localization
+    : Associative plus_rng_localization.
+  Proof.
+    srapply Quotient_ind3_hprop; intros x y z.
+    apply qglue, fraction_eq_simple.
+    simpl.
+    rewrite ? rng_dist_r.
+    rewrite ? rng_mult_assoc.
+    rewrite ? rng_plus_assoc.
+    do 4 f_ap.
+    all: rewrite <- ? rng_mult_assoc.
+    all: f_ap.
+    2: apply rng_mult_comm.
+    rewrite rng_mult_assoc.
+    apply rng_mult_comm.
+  Defined.
+
+  Instance leftidentity_mult_rng_localization
+    : LeftIdentity mult_rng_localization one_rng_localization.
+  Proof.
+    srapply Quotient_ind_hprop; intros f.
+    apply qglue, fraction_eq_simple; simpl.
+    f_ap; [|symmetry]; apply rng_mult_one_l.
+  Defined.
+
+  Instance associative_mult_rng_localization
+    : Associative mult_rng_localization.
+  Proof.
+    srapply Quotient_ind3_hprop; intros x y z.
+    apply qglue, fraction_eq_simple.
+    f_ap; [|symmetry]; apply rng_mult_assoc.
+  Defined.
+
+  Instance commutative_mult_rng_localization
+    : Commutative mult_rng_localization.
+  Proof.
+    srapply Quotient_ind2_hprop; intros x y.
+    apply qglue, fraction_eq_simple; simpl.
+    f_ap; rapply rng_mult_comm.
+  Defined.
+
+  Instance leftdistribute_rng_localization
+    : LeftDistribute mult_rng_localization plus_rng_localization.
+  Proof.
+    srapply Quotient_ind3_hprop; intros x y z.
+    apply qglue, fraction_eq_simple.
+    simpl.
+    rewrite ? rng_dist_l, ? rng_dist_r.
+    rewrite ? rng_mult_assoc.
+    do 2 f_ap.
+    all: rewrite <- ? rng_mult_assoc.
+    all: do 2 f_ap.
+    all: rewrite ? rng_mult_assoc.
+    all: rewrite (rng_mult_comm (_ x)).
+    all: rewrite <- ? rng_mult_assoc.
+    all: f_ap.
+    all: rewrite (rng_mult_comm _ (_ y)).
+    all: rewrite <- ? rng_mult_assoc.
+    all: f_ap.
+  Defined.
+
+  Definition rng_localization : CRing.
+  Proof.
+    snrapply Build_CRing'.
+    1: rapply (Build_AbGroup' (Quotient fraction_eq)).
+    all: exact _.
+  Defined.
+
+  Definition loc_in : R $-> rng_localization.
+  Proof.
+    snrapply Build_RingHomomorphism.
+    1: exact (class_of _ o frac_in).
+    snrapply Build_IsSemiRingPreserving.
+    - snrapply Build_IsMonoidPreserving.
+      + intros x y.
+        snrapply qglue.
+        apply fraction_eq_simple.
+        by simpl; rewrite 5 rng_mult_one_r.
+      + reflexivity.
+    - snrapply Build_IsMonoidPreserving.
+      + intros x y.
+        snrapply qglue.
+        apply fraction_eq_simple.
+        by simpl; rewrite 3 rng_mult_one_r.
+      + reflexivity.
+  Defined.
+  
+  Section Rec.
+
+    Context (T : CRing) (f : R $-> T)
+      (H : forall x, S x -> IsInvertible T (f x)).
+
+    Definition rng_localization_rec_map : rng_localization -> T.
+    Proof.
+      srapply Quotient_rec.
+      - intros [n d sd].
+        refine (f n * inverse_elem (f d)).
+        exact (H d sd).
+      - simpl.
+        intros x y z.
+        apply rng_inv_moveR_rV.
+        rhs_V nrapply rng_mult_move_left_assoc.
+        rhs_V nrapply rng_mult_assoc.
+        apply rng_inv_moveL_Vr.
+        lhs_V nrapply rng_homo_mult.
+        rhs_V nrapply rng_homo_mult.
+        nrapply (equiv_inj (f z.1 *.)).
+        { nrapply isequiv_rng_inv_mult_l.
+          exact (H _ (fst z.2)). }
+        lhs_V nrapply rng_homo_mult.
+        rhs_V nrapply rng_homo_mult.
+        lhs nrapply ap.
+        1: lhs nrapply rng_mult_assoc.
+        1: nrapply rng_mult_permute_2_3.
+        rhs nrapply ap.
+        2: nrapply rng_mult_assoc.
+        exact (ap f (snd z.2)).
+    Defined.
+
+    Instance issemiringpreserving_rng_localization_rec_map
+      : IsSemiRingPreserving rng_localization_rec_map.
+    Proof.
+      snrapply Build_IsSemiRingPreserving.
+      - snrapply Build_IsMonoidPreserving.
+        + srapply Quotient_ind2_hprop.
+          intros x y; simpl.
+          apply rng_inv_moveR_rV.
+          rhs nrapply rng_dist_r.
+          rewrite rng_homo_plus.
+          rewrite 3 rng_homo_mult.
+          f_ap.
+          1,2: rhs_V nrapply rng_mult_assoc.
+          1,2: f_ap.
+          1,2: lhs_V nrapply rng_mult_one_l.
+          1,2: rhs nrapply rng_mult_assoc.
+          2: rhs nrapply rng_mult_comm.
+          2: rhs nrapply rng_mult_assoc.
+          1,2: f_ap.
+          1,2: symmetry.
+          * apply rng_inv_l.
+          * apply rng_inv_r. 
+        + hnf; simpl. rewrite rng_homo_zero.
+          nrapply rng_mult_zero_l.
+      - snrapply Build_IsMonoidPreserving.
+        + srapply Quotient_ind2_hprop.
+          intros x y; simpl.
+          apply rng_inv_moveR_rV.
+          lhs nrapply rng_homo_mult.
+          rhs_V nrapply rng_mult_assoc.
+          rhs_V nrapply rng_mult_assoc.
+          apply ap.
+          apply rng_inv_moveL_Vr.
+          lhs nrapply rng_mult_comm.
+          rhs_V nrapply rng_mult_assoc.
+          apply ap.
+          apply rng_inv_moveL_Vr.
+          symmetry.
+          rhs nrapply rng_mult_comm.
+          nrapply rng_homo_mult.
+        + apply rng_inv_moveR_rV; symmetry.
+          apply rng_mult_one_l.
+    Defined.
+
+    Definition rng_localization_rec : rng_localization $-> T
+      := Build_RingHomomorphism rng_localization_rec_map _.
+    
+    Definition rng_localization_rec_beta
+      : rng_localization_rec $o loc_in $== f.
+    Proof.
+      intros x; simpl.   
+      apply rng_inv_moveR_rV.
+      lhs_V nrapply rng_mult_one_r.
+      nrapply ap; symmetry.
+      apply rng_homo_one.
+    Defined.
+  
+  End Rec.
+  
+  (** Elements belonging to the multiplicative subset [S] of [R] become invertible in [rng_localization R S]. *)
+  Global Instance isinvertible_rng_localization (x : R) (Sx : S x)
+    : IsInvertible rng_localization (loc_in x).
+  Proof.
+    snrapply isinvertible_cring.
+    - exact (class_of _ (Build_Fraction 1 x Sx)).
+    - apply qglue, fraction_eq_simple.
+      exact (rng_mult_assoc _ _ _)^.
+  Defined.
+  
+  (** As a special case, any denominator of a fraction must necessarily be invertible. *)
+  Global Instance isinvertible_denominator (f : Fraction)
+    : IsInvertible rng_localization (loc_in (denominator f)).
+  Proof.
+    snrapply isinvertible_rng_localization.
+    exact (in_mult_subset_denominator f).
+  Defined.
+  
+  (** Elements that were invertible in the original ring [R], continue to be invertible in [rng_localization R S]. Since [loc_in] is a ring homomorphism this is automatic. *)
+  Definition isinvertible_rng_localization_preserved (x : R)
+    : IsInvertible R x -> IsInvertible rng_localization (loc_in x)
+    := _.
+  
+  (** We can factor any fraction as the multiplication of the numerator and the inverse of the denominator. *)
+  Definition fraction_decompose (f : Fraction)
+    : class_of fraction_eq f
+      = loc_in (numerator f) * inverse_elem (loc_in (denominator f)).
+  Proof.
+    apply qglue, fraction_eq_simple.
+    nrapply rng_mult_assoc.
+  Defined.
+
+  Definition rng_localization_ind
+    (P : rng_localization -> Type)
+    (H : forall x, IsHProp (P x))
+    (Hin : forall x, P (loc_in x))
+    (Hinv : forall x (H : IsInvertible rng_localization x),
+      P x -> P (inverse_elem x))
+    (Hmul : forall x y, P x -> P y -> P (x * y))
+    : forall x, P x.
+  Proof.
+    srapply Quotient_ind.
+    - intros f.
+      refine (transport P (fraction_decompose f)^ _).
+      apply Hmul.
+      + apply Hin.
+      + apply Hinv, Hin.
+    - intros f1 f2 p.
+      apply path_ishprop.
+  Defined.
+  
+  Definition rng_localization_ind_homotopy {T : CRing}
+    {f g : rng_localization $-> T}
+    (p : f $o loc_in $== g $o loc_in)
+    : f $== g.
+  Proof.
+    srapply rng_localization_ind.
+    - exact p.
+    - hnf; intros x H q.
+      change (inverse_elem (f x) = inverse_elem (g x)).
+      apply isinvertible_unique.
+      exact q.
+    - hnf; intros x y q r.
+      lhs nrapply rng_homo_mult.
+      rhs nrapply rng_homo_mult.
+      f_ap.
+  Defined.
+
+End Localization.
+
+(** TODO: Show construction is a localization. *)
diff --git a/theories/Algebra/Rings/QuotientRing.v b/theories/Algebra/Rings/QuotientRing.v
index caeec5bcb26..514c3a1a99f 100644
--- a/theories/Algebra/Rings/QuotientRing.v
+++ b/theories/Algebra/Rings/QuotientRing.v
@@ -40,23 +40,11 @@ Section QuotientRing.
 
   Instance mult_quotient_group : Mult (QuotientAbGroup R I).
   Proof.
-    intro x.
-    srapply Quotient_rec.
-    { intro y; revert x.
-      srapply Quotient_rec.
-      { intro x.
-        apply class_of.
-        exact (x * y). }
-      intros x x' p.
+    srapply Quotient_rec2.
+    - exact (fun x y => class_of _ (x * y)).
+    - intros x x' p y y' q; simpl.
       apply qglue.
-      by rapply iscong. }
-    intros y y' q.
-    revert x.
-    srapply Quotient_ind_hprop.
-    intro x.
-    simpl.
-    apply qglue.
-    by rapply iscong.
+      by rapply iscong.
   Defined.
 
   Instance one_quotient_abgroup : One (QuotientAbGroup R I) := class_of _ one.
@@ -68,10 +56,7 @@ Section QuotientRing.
     1: repeat split.
     1: exact _.
     (** Associativity follows from the underlying operation *)
-    { intros x y.
-      snrapply Quotient_ind_hprop; [exact _ | intro z; revert y].
-      snrapply Quotient_ind_hprop; [exact _ | intro y; revert x].
-      snrapply Quotient_ind_hprop; [exact _ | intro x ].
+    { srapply Quotient_ind3_hprop; intros x y z.
       unfold sg_op, mult_is_sg_op, mult_quotient_group; simpl.
       apply ap.
       apply associativity. }
@@ -82,18 +67,12 @@ Section QuotientRing.
     1: apply left_identity.
     1: apply right_identity.
     (** Finally distributivity also follows *)
-    { intros x y.
-      snrapply Quotient_ind_hprop; [exact _ | intro z; revert y].
-      snrapply Quotient_ind_hprop; [exact _ | intro y; revert x].
-      snrapply Quotient_ind_hprop; [exact _ | intro x ].
+    { srapply Quotient_ind3_hprop; intros x y z.
       unfold sg_op, mult_is_sg_op, mult_quotient_group,
         plus, mult, plus_quotient_group; simpl.
       apply ap.
       apply simple_distribute_l. }
-    { intros x y.
-      snrapply Quotient_ind_hprop; [exact _ | intro z; revert y].
-      snrapply Quotient_ind_hprop; [exact _ | intro y; revert x].
-      snrapply Quotient_ind_hprop; [exact _ | intro x ].
+    { srapply Quotient_ind3_hprop; intros x y z.
       unfold sg_op, mult_is_sg_op, mult_quotient_group,
         plus, mult, plus_quotient_group; simpl.
       apply ap.
@@ -138,7 +117,26 @@ Definition QuotientRing_ind_hprop {R : Ring} {I : Ideal R} (P : R / I -> Type)
   : forall (r : R / I), P r
   := Quotient_ind_hprop _ P c.
 
-(** ** Quotient thoery *)
+Definition QuotientRing_ind2_hprop {R : Ring} {I : Ideal R} (P : R / I -> R / I -> Type)
+  `{forall x y, IsHProp (P x y)}
+  (c : forall (x y : R), P (rng_quotient_map I x) (rng_quotient_map I y))
+  : forall (r s : R / I), P r s
+  := Quotient_ind2_hprop _ P c.
+
+Definition QuotientRing_rec {R : Ring} {I : Ideal R} (S : Ring)
+  (f : R $-> S) (H : forall x, I x -> f x = 0) 
+  : R / I $-> S.
+Proof.
+  snrapply Build_RingHomomorphism'.
+  - snrapply (grp_quotient_rec _ _ f).
+    exact H.
+  - split.
+    + srapply QuotientRing_ind2_hprop.
+      nrapply rng_homo_mult.
+    + nrapply rng_homo_one.
+Defined.
+
+(** ** Quotient theory *)
 
 (** First isomorphism theorem for commutative rings *)
 Definition rng_first_iso `{Funext} {A B : Ring} (f : A $-> B)
@@ -147,9 +145,7 @@ Proof.
   snrapply Build_RingIsomorphism''.
   1: rapply abgroup_first_iso.
   split.
-  { intros x y.
-    revert y; srapply QuotientRing_ind_hprop; intros y.
-    revert x; srapply QuotientRing_ind_hprop; intros x.
+  { srapply QuotientRing_ind2_hprop; intros x y.
     srapply path_sigma_hprop.
     exact (rng_homo_mult _ _ _). }
   srapply path_sigma_hprop.
@@ -166,11 +162,7 @@ Proof.
     intros x y; cbn.
     apply p. }
   repeat split.
-  1,2: intros x; simpl.
-  1,2: srapply QuotientRing_ind_hprop.
-  1,2: intros y; revert x.
-  1,2: srapply QuotientRing_ind_hprop.
-  1,2: intros x; rapply qglue.
+  1,2: srapply Quotient_ind2_hprop; intros x y; rapply qglue.
   1: change (J ( - (x + y) + (x + y))).
   2: change (J (- ( x * y) + (x * y))).
   1,2: rewrite rng_plus_negate_l.
diff --git a/theories/Algebra/Rings/Ring.v b/theories/Algebra/Rings/Ring.v
index ab438bf8fcb..da5d0134355 100644
--- a/theories/Algebra/Rings/Ring.v
+++ b/theories/Algebra/Rings/Ring.v
@@ -93,6 +93,7 @@ Section RingLaws.
 
   Definition rng_negate_negate : - (- x) = x := groups.negate_involutive _.
   Definition rng_negate_zero : - (0 : A) = 0 := groups.negate_mon_unit.
+  Definition rng_negate_plus : - (x + y) = - x - y := negate_plus_distr _ _.
 
   Definition rng_mult_one_l : 1 * x = x := left_identity _.
   Definition rng_mult_one_r : x * 1 = x := right_identity _.
@@ -105,6 +106,22 @@ Section RingLaws.
 
 End RingLaws.
 
+Definition rng_dist_l_negate {A : Ring} (x y z : A)
+  : x * (y - z) = x * y - x * z.
+Proof.
+  lhs nrapply rng_dist_l.
+  nrapply ap.
+  nrapply rng_mult_negate_r.
+Defined.
+
+Definition rng_dist_r_negate {A : Ring} (x y z : A)
+  : (x - y) * z = x * z - y * z.
+Proof.
+  lhs nrapply rng_dist_r.
+  nrapply ap.
+  nrapply rng_mult_negate_l.
+Defined.
+
 Section RingHomoLaws.
 
   Context {A B : Ring} (f : RingHomomorphism A B) (x y : A).
@@ -616,6 +633,15 @@ Proof.
     by exists (inv : rng_op R).
 Defined.
 
+(** The invertible elements in [R] and [rng_op R] agree, by swapping the proofs of left and right invertibility. *)
+Definition isinvertible_rng_op (R : Ring) (x : R) `{!IsInvertible R x}
+  : IsInvertible (rng_op R) x.
+Proof.
+  split.
+  - exact (isrightinvertible_isinvertible).
+  - exact (isleftinvertible_isinvertible).
+Defined.
+
 (** *** Uniqueness of inverses *)
 
 (** This general lemma will be used for uniqueness results. *)
@@ -661,10 +687,11 @@ Proof.
   apply path_left_inverse_elem_right_inverse_elem.
 Defined.
 
-(** Furthermore, any two proofs of invertibility have the same inverse. *)
-Definition isinvertible_unique {R x} (H1 H2 : IsInvertible R x)
-  : @inverse_elem R x H1 = @inverse_elem R x H2.
+(** Equal elements have equal inverses.  Note that we don't require that the proofs of invertibility are equal (over [p]).  It follows that the inverse of an invertible element [x] depends only on [x]. *)
+Definition isinvertible_unique {R : Ring} (x y : R) `{IsInvertible R x} `{IsInvertible R y} (p : x = y)
+  : inverse_elem x = inverse_elem y.
 Proof.
+  destruct p.
   snrapply (path_left_right_inverse x).
   - apply rng_inv_l.
   - apply rng_inv_r.
@@ -761,16 +788,24 @@ Proof.
   exact (right_inverse_eq x).
 Defined.
 
-(** Inverses of invertible elements are themselves invertible. *)
+(** Inverses of invertible elements are themselves invertible.  We take both inverses of [inverse_elem x] to be [x]. *)
 Global Instance isinvertible_inverse_elem {R : Ring} (x : R)
   `{IsInvertible R x}
   : IsInvertible R (inverse_elem x).
 Proof.
   split.
-  - unfold inverse_elem.
-    rewrite (path_left_inverse_elem_right_inverse_elem x).
-    exact _.
-  - exact _.
+  - exists x; apply rng_inv_r.
+  - apply isrightinvertible_left_inverse_elem.
+Defined.
+
+(** Since [inverse_elem (inverse_elem x) = x], we get the following equivalence. *)
+Definition equiv_path_inverse_elem {R : Ring} {x y : R}
+  `{IsInvertible R x, IsInvertible R y}
+  : x = y <~> inverse_elem x = inverse_elem y.
+Proof.
+  srapply equiv_iff_hprop.
+  - exact (isinvertible_unique x y).
+  - exact (isinvertible_unique (inverse_elem x) (inverse_elem y)).
 Defined.
 
 (** [1] is always invertible, and by the above [-1]. *)
@@ -782,10 +817,24 @@ Proof.
   - apply rng_mult_one_l.
 Defined.
 
+(** Ring homomorphisms preserve invertible elements. *)
+Global Instance isinvertible_rng_homo {R S} (f : R $-> S)
+  : forall x, IsInvertible R x -> IsInvertible S (f x).
+Proof.
+  intros x H.
+  snrapply Build_IsInvertible.
+  1: exact (f (inverse_elem x)).
+  1,2: lhs_V nrapply rng_homo_mult.
+  1,2: rhs_V nrapply (rng_homo_one f).
+  1,2: nrapply (ap f).
+  - exact (rng_inv_l x).
+  - exact (rng_inv_r x).
+Defined.
+
 (** *** Group of units *)
 
 (** Invertible elements are typically called "units" in ring theory and the collection of units forms a group under the ring multiplication. *)
-Definition rng_unit_group {R : Ring} : Group.
+Definition rng_unit_group (R : Ring) : Group.
 Proof.
   (** TODO: Use a generalised version of [Build_Subgroup] that works for subgroups of monoids. *)
   snrapply Build_Group.
@@ -808,4 +857,55 @@ Proof.
     + apply rng_inv_r.
 Defined.
 
+(** *** Multiplication by an invertible element is an equivalence *)
+
+Global Instance isequiv_rng_inv_mult_l {R : Ring} {x : R}
+  `{IsInvertible R x}
+  : IsEquiv (x *.).
+Proof.
+  snrapply isequiv_adjointify.
+  1: exact (inverse_elem x *.).
+  1,2: intros y.
+  1,2: lhs nrapply rng_mult_assoc.
+  1,2: rhs_V nrapply rng_mult_one_l.
+  1,2: snrapply (ap (.* y)).
+  - nrapply rng_inv_r.
+  - nrapply rng_inv_l.
+Defined.
+
+(** This can be proved by combining [isequiv_rng_inv_mult_l (R:=rng_op R)] with [isinvertible_rng_op], but then the inverse map is given by multiplying by [right_inverse_elem x] not [inverse_elem x], which complicates calculations. *)
+Global Instance isequiv_rng_inv_mult_r {R : Ring} {x : R}
+  `{IsInvertible R x}
+  : IsEquiv (.* x).
+Proof.
+  snrapply isequiv_adjointify.
+  1: exact (.* inverse_elem x).
+  1,2: intros y.
+  1,2: lhs_V nrapply rng_mult_assoc.
+  1,2: rhs_V nrapply rng_mult_one_r.
+  1,2: snrapply (ap (y *.)).
+  - nrapply rng_inv_l.
+  - nrapply rng_inv_r.
+Defined.
+
+(** *** Invertible element movement lemmas *)
+
+(** These cannot be proven using the corresponding group laws in the group of units since not all elements involved are invertible. *)
+
+Definition rng_inv_moveL_Vr {R : Ring} {x y z : R} `{IsInvertible R y}
+  : y * x = z <~> x = inverse_elem y * z
+  := equiv_moveL_equiv_V (f := (y *.)) z x.
+
+Definition rng_inv_moveL_rV {R : Ring} {x y z : R} `{IsInvertible R y}
+  : x * y = z <~> x = z * inverse_elem y
+  := equiv_moveL_equiv_V (f := (.* y)) z x.
+
+Definition rng_inv_moveR_Vr {R : Ring} {x y z : R} `{IsInvertible R y}
+  : x = y * z <~> inverse_elem y * x = z
+  := equiv_moveR_equiv_V (f := (y *.)) x z.
+
+Definition rng_inv_moveR_rV {R : Ring} {x y z : R} `{IsInvertible R y}
+  : x = z * y <~> x * inverse_elem y = z
+  := equiv_moveR_equiv_V (f := (.* y)) x z.
+
 (** TODO: The group of units construction is a functor from [Ring -> Group] and is right adjoint to the group ring construction. *)
diff --git a/theories/Algebra/Rings/Z.v b/theories/Algebra/Rings/Z.v
index 8f8c8a25098..0d9cf3b124b 100644
--- a/theories/Algebra/Rings/Z.v
+++ b/theories/Algebra/Rings/Z.v
@@ -10,16 +10,13 @@ Require Import WildCat.Core.
 Definition cring_Z : CRing.
 Proof.
   snrapply Build_CRing'.
-  6: repeat split.
   - exact abgroup_Z.
   - exact 1%int.
   - exact int_mul.
   - exact int_mul_comm.
-  - exact int_dist_l.
-  - exact _.
   - exact int_mul_assoc.
+  - exact int_dist_l.
   - exact int_mul_1_l.
-  - exact int_mul_1_r.
 Defined.
 
 Local Open Scope mc_scope.
diff --git a/theories/Colimits/Quotient.v b/theories/Colimits/Quotient.v
index e3c8f4b7b3d..3ee2c9cb201 100644
--- a/theories/Colimits/Quotient.v
+++ b/theories/Colimits/Quotient.v
@@ -17,7 +17,9 @@ Inductive Quotient R : Type :=
    | qglue : forall x y, (R x y) -> class_of R x = class_of R y
    | ishset_quotient : IsHSet (Quotient R)
 >>
-We do this by defining the quotient as a 0-truncated graph quotient. *)
+We do this by defining the quotient as a 0-truncated graph quotient. 
+
+Throughout this file [a], [b] and [c] are elements of [A], [R] is a relation on [A], [x], [y] and [z] are elements of [Quotient R], [p] is a proof of [R a b]. *)
 
 Definition Quotient@{i j k} {A : Type@{i}} (R : Relation@{i j} A) : Type@{k}
   := Trunc@{k} 0 (GraphQuotient@{i j k} R).
@@ -25,39 +27,37 @@ Definition Quotient@{i j k} {A : Type@{i}} (R : Relation@{i j} A) : Type@{k}
 Definition class_of@{i j k} {A : Type@{i}} (R : Relation@{i j} A)
   : A -> Quotient@{i j k} R := tr o gq.
 
-Definition qglue@{i j k} {A : Type@{i}} {R : Relation@{i j} A}
-  {x y : A}
-  : R x y -> class_of@{i j k} R x = class_of R y
+Definition qglue@{i j k} {A : Type@{i}} {R : Relation@{i j} A} {a b : A}
+  : R a b -> class_of@{i j k} R a = class_of R b
   := fun p => ap tr (gqglue p).
 
 Global Instance ishset_quotient {A : Type} (R : Relation A)
   : IsHSet (Quotient R) := _.
 
-Definition Quotient_ind@{i j k l}
-  {A : Type@{i}} (R : Relation@{i j} A)
+Definition Quotient_ind@{i j k l} {A : Type@{i}} (R : Relation@{i j} A)
   (P : Quotient@{i j k} R -> Type@{l}) {sP : forall x, IsHSet (P x)}
-  (pclass : forall x, P (class_of R x))
-  (peq : forall x y (H : R x y), qglue H # pclass x = pclass y)
-  : forall q, P q.
+  (pclass : forall a, P (class_of R a))
+  (peq : forall a b (H : R a b), qglue H # pclass a = pclass b)
+  : forall x, P x.
 Proof.
-  eapply Trunc_ind, GraphQuotient_ind.
-  1: assumption.
-  intros a b p.
-  refine (transport_compose _ _ _ _ @ _).
-  apply peq.
+  rapply Trunc_ind; srapply GraphQuotient_ind.
+  - exact pclass.
+  - intros a b p.
+    lhs nrapply (transport_compose P).
+    exact (peq a b p).
 Defined.
 
 Definition Quotient_ind_beta_qglue@{i j k l}
   {A : Type@{i}} (R : Relation@{i j} A)
   (P : Quotient@{i j k} R -> Type@{l}) {sP : forall x, IsHSet (P x)}
-  (pclass : forall x, P (class_of R x))
-  (peq : forall x y (H : R x y), qglue H # pclass x = pclass y)
-  (x y : A) (p : R x y)
-  : apD (Quotient_ind@{i j k l} R P pclass peq) (qglue p) = peq x y p.
+  (pclass : forall a, P (class_of R a))
+  (peq : forall a b (H : R a b), qglue H # pclass a = pclass b)
+  (a b : A) (p : R a b)
+  : apD (Quotient_ind@{i j k l} R P pclass peq) (qglue p) = peq a b p.
 Proof.
-  refine (apD_compose' tr _ _ @ _).
+  lhs nrapply apD_compose'.
   unfold Quotient_ind.
-  refine (ap _ (GraphQuotient_ind_beta_gqglue _ pclass
+  nrefine (ap _ (GraphQuotient_ind_beta_gqglue _ pclass
     (fun a b p0 => transport_compose P tr _ _ @ peq a b p0) _ _ _) @ _).
   rapply concat_V_pp.
 Defined.
@@ -65,22 +65,23 @@ Defined.
 Definition Quotient_rec@{i j k l}
   {A : Type@{i}} (R : Relation@{i j} A)
   (P : Type@{l}) `{IsHSet P} (pclass : A -> P)
-  (peq : forall x y, R x y -> pclass x = pclass y)
+  (peq : forall a b, R a b -> pclass a = pclass b)
   : Quotient@{i j k} R -> P.
 Proof.
-  eapply Trunc_rec, GraphQuotient_rec.
-  apply peq.
+  srapply Trunc_rec; snrapply GraphQuotient_rec.
+  - exact pclass.
+  - exact peq.
 Defined.
 
 Definition Quotient_rec_beta_qglue @{i j k l}
   {A : Type@{i}} (R : Relation@{i j} A)
   (P : Type@{l}) `{IsHSet P} (pclass : A -> P)
-  (peq : forall x y, R x y -> pclass x = pclass y)
-  (x y : A) (p : R x y)
-  : ap (Quotient_rec@{i j k l} R P pclass peq) (qglue p) = peq x y p.
+  (peq : forall a b, R a b -> pclass a = pclass b)
+  (a b : A) (p : R a b)
+  : ap (Quotient_rec@{i j k l} R P pclass peq) (qglue p) = peq a b p.
 Proof.
-  refine ((ap_compose tr _ _)^ @ _).
-  srapply GraphQuotient_rec_beta_gqglue.
+  lhs_V nrapply (ap_compose tr).
+  snrapply GraphQuotient_rec_beta_gqglue.
 Defined.
 
 Arguments Quotient : simpl never.
@@ -91,6 +92,36 @@ Arguments Quotient_rec_beta_qglue : simpl never.
 
 Notation "A / R" := (Quotient (A:=A) R).
 
+(* Quotient induction into a hprop. *)
+Definition Quotient_ind_hprop {A : Type@{i}} (R : Relation@{i j} A)
+  (P : A / R -> Type) `{forall x, IsHProp (P x)}
+  (dclass : forall a, P (class_of R a))
+  : forall x, P x.
+Proof.
+  srapply (Quotient_ind R P dclass).
+  intros x y p; apply path_ishprop.
+Defined.
+
+Definition Quotient_ind2_hprop {A : Type@{i}} (R : Relation@{i j} A)
+  (P : A / R -> A / R -> Type) `{forall x y, IsHProp (P x y)}
+  (dclass : forall a b, P (class_of R a) (class_of R b))
+  : forall x y, P x y.
+Proof.
+  intros x; srapply Quotient_ind_hprop; intros b.
+  revert x; srapply Quotient_ind_hprop; intros a.
+  exact (dclass a b).
+Defined.
+
+Definition Quotient_ind3_hprop {A : Type@{i}} (R : Relation@{i j} A)
+  (P : A / R -> A / R -> A / R -> Type) `{forall x y z, IsHProp (P x y z)}
+  (dclass : forall a b c, P (class_of R a) (class_of R b) (class_of R c))
+  : forall x y z, P x y z.
+Proof.
+  intros x; srapply Quotient_ind2_hprop; intros b c.
+  revert x; srapply Quotient_ind_hprop; intros a.
+  exact (dclass a b c).
+Defined.
+
 Section Equiv.
 
   Context `{Univalence} {A : Type} (R : Relation A) `{is_mere_relation _ R}
@@ -99,95 +130,76 @@ Section Equiv.
   (* The proposition of being in a given class in a quotient. *)
   Definition in_class : A / R -> A -> HProp.
   Proof.
-    srapply Quotient_ind.
-    { intros a b.
-      exact (Build_HProp (R a b)). }
-    intros x y p.
-    refine (transport_const _ _ @ _).
-    funext z.
+    intros x b; revert x.
+    srapply Quotient_rec.
+    1: intro a; exact (Build_HProp (R a b)).
+    intros a c p; cbn beta.
     apply path_hprop.
     srapply equiv_iff_hprop; cbn.
     1: apply (transitivity (symmetry _ _ p)).
     apply (transitivity p).
   Defined.
 
-  (* Quotient induction into a hprop. *)
-  Definition Quotient_ind_hprop
-    (P : A / R -> Type) `{forall x, IsHProp (P x)}
-    (dclass : forall x, P (class_of R x)) : forall q, P q.
-  Proof.
-    srapply (Quotient_ind R P dclass).
-    all: try (intro; apply trunc_succ).
-    intros x y p.
-    apply path_ishprop.
-  Defined.
-
   (* Being in a class is decidable if the Relation is decidable. *)
-  Global Instance decidable_in_class `{forall x y, Decidable (R x y)}
+  Global Instance decidable_in_class `{forall a b, Decidable (R a b)}
   : forall x a, Decidable (in_class x a).
   Proof.
     by srapply Quotient_ind_hprop.
   Defined.
 
   (* if x is in a class q, then the class of x is equal to q. *)
-  Lemma path_in_class_of : forall q x, in_class q x -> q = class_of R x.
+  Lemma path_in_class_of : forall x a, in_class x a -> x = class_of R a.
   Proof.
     srapply Quotient_ind.
     { intros x y p.
-      apply (qglue p). }
+      exact (qglue p). }
     intros x y p.
     funext ? ?.
     apply hset_path2.
   Defined.
 
-  Lemma related_quotient_paths : forall x y,
-    class_of R x = class_of R y -> R x y.
+  Lemma related_quotient_paths (a b : A)
+    : class_of R a = class_of R b -> R a b.
   Proof.
-    intros x y p.
-    change (in_class (class_of R x) y).
+    intros p.
+    change (in_class (class_of R a) b).
     destruct p^.
     cbv; reflexivity.
   Defined.
 
   (** Thm 10.1.8 *)
-  Theorem path_quotient : forall x y,
-    R x y <~> (class_of R x = class_of R y).
+  Theorem path_quotient (a b : A)
+    : R a b <~> (class_of R a = class_of R b).
   Proof.
-    intros ??.
     apply equiv_iff_hprop.
     - apply qglue.
     - apply related_quotient_paths.
   Defined.
 
-  Definition Quotient_rec2 `{Funext} {B : HSet} {dclass : A -> A -> B}
-    {dequiv : forall x x', R x x' -> forall y y',
-      R y y' -> dclass x y = dclass x' y'}
+  Definition Quotient_rec2 {B : Type} `{IsHSet B} {dclass : A -> A -> B}
+    {dequiv : forall a a', R a a' -> forall b b',
+      R b b' -> dclass a b = dclass a' b'}
     : A / R -> A / R -> B.
   Proof.
+    clear H. (* Ensure that we don't use Univalence. *)
+    intro x.
     srapply Quotient_rec.
-    { intro a.
+    - intro b.
+      revert x.
       srapply Quotient_rec.
-      { revert a.
-        assumption. }
-      by apply (dequiv a a). }
-    intros x y p.
-    apply path_forall.
-    srapply Quotient_ind.
-    { cbn; intro a.
-      by apply dequiv. }
-    intros a b q.
-    apply path_ishprop.
-  Defined.
-
-  Definition Quotient_ind_hprop' (P : A / R -> Type)
-    `{forall x, IsHProp (P (class_of _ x))}
-    (dclass : forall x, P (class_of _ x)) : forall y, P y.
-  Proof.
-    apply Quotient_ind with dclass.
-    { srapply Quotient_ind.
-      1: intro; apply istrunc_succ.
-      intros ???; apply path_ishprop. }
-    intros; apply path_ishprop.
+      + intro a.
+        exact (dclass a b).
+      + cbn beta.
+        intros a a' p.
+        by apply (dequiv a a' p b b).
+    - cbn beta.
+      intros b b' p.
+      revert x.
+      srapply Quotient_ind.
+      + cbn; intro a.
+        by apply dequiv.
+      + intros a a' q.
+        apply path_ishprop.
   Defined.
 
   (** The map class_of : A -> A/R is a surjection. *)
@@ -195,15 +207,15 @@ Section Equiv.
   Proof.
     apply BuildIsSurjection.
     srapply Quotient_ind_hprop.
-    intro x.
+    intro a.
     apply tr.
-    by exists x.
+    by exists a.
   Defined.
 
   (* Universal property of quotient *)
   (* Lemma 6.10.3 *)
-  Theorem equiv_quotient_ump (B : HSet)
-    : (A / R -> B) <~> {f : A -> B & forall x y, R x y -> f x = f y}.
+  Theorem equiv_quotient_ump (B : Type) `{IsHSet B}
+    : (A / R -> B) <~> {f : A -> B & forall a b, R a b -> f a = f b}.
   Proof.
     srapply equiv_adjointify.
     + intro f.
@@ -240,12 +252,12 @@ Section Functoriality.
   Definition Quotient_functor
     {A : Type} (R : Relation A)
     {B : Type} (S : Relation B)
-    (f : A -> B) (fresp : forall x y, R x y -> S (f x) (f y))
+    (f : A -> B) (fresp : forall a b, R a b -> S (f a) (f b))
     : Quotient R -> Quotient S.
   Proof.
     refine (Quotient_rec R _ (class_of S o f) _).
-    intros x y r.
-    apply qglue, fresp, r.
+    intros a b p.
+    apply qglue, fresp, p.
   Defined.
 
   Definition Quotient_functor_idmap
@@ -259,9 +271,9 @@ Section Functoriality.
     {A : Type} {R : Relation A}
     {B : Type} {S : Relation B}
     {C : Type} {T : Relation C}
-    (f : A -> B) (fresp : forall x y, R x y -> S (f x) (f y))
-    (g : B -> C) (gresp : forall x y, S x y -> T (g x) (g y))
-    : Quotient_functor R T (g o f) (fun x y => (gresp _ _) o (fresp x y))
+    (f : A -> B) (fresp : forall a b, R a b -> S (f a) (f b))
+    (g : B -> C) (gresp : forall a b, S a b -> T (g a) (g b))
+    : Quotient_functor R T (g o f) (fun a b => (gresp _ _) o (fresp a b))
     == Quotient_functor S T g gresp o Quotient_functor R S f fresp.
   Proof.
     by srapply Quotient_ind_hprop.
@@ -271,11 +283,11 @@ Section Functoriality.
           {B : Type} (S : Relation B).
 
   Global Instance isequiv_quotient_functor (f : A -> B)
-    (fresp : forall x y, R x y <-> S (f x) (f y)) `{IsEquiv _ _ f}
-    : IsEquiv (Quotient_functor R S f (fun x y => fst (fresp x y))).
+    (fresp : forall a b, R a b <-> S (f a) (f b)) `{IsEquiv _ _ f}
+    : IsEquiv (Quotient_functor R S f (fun a b => fst (fresp a b))).
   Proof.
     srapply (isequiv_adjointify _ (Quotient_functor S R f^-1 _)).
-    { intros u v s.
+    { intros a b s.
       apply (snd (fresp _ _)).
       abstract (do 2 rewrite eisretr; apply s). }
     all: srapply Quotient_ind.
@@ -288,12 +300,12 @@ Section Functoriality.
   Defined.
 
   Definition equiv_quotient_functor (f : A -> B) `{IsEquiv _ _ f}
-    (fresp : forall x y, R x y <-> S (f x) (f y))
+    (fresp : forall a b, R a b <-> S (f a) (f b))
     : Quotient R <~> Quotient S
-    := Build_Equiv _ _ (Quotient_functor R S f (fun x y => fst (fresp x y))) _.
+    := Build_Equiv _ _ (Quotient_functor R S f (fun a b => fst (fresp a b))) _.
 
   Definition equiv_quotient_functor' (f : A <~> B)
-    (fresp : forall x y, R x y <-> S (f x) (f y))
+    (fresp : forall a b, R a b <-> S (f a) (f b))
     : Quotient R <~> Quotient S
     := equiv_quotient_functor f fresp.
 
@@ -358,7 +370,7 @@ Definition quotient_kernel_factor@{a b ab ab' | a <= ab, b <= ab, ab < ab'}
       IsHSet C * IsSurjection e * IsEmbedding m * (f = m o e).
 Proof.
   exact (quotient_kernel_factor_general@{a b ab ab' b ab ab}
-           f (fun x y => f x = f y) (fun x y => equiv_idmap)).
+           f (fun a b => f a = f b) (fun x y => equiv_idmap)).
 Defined.
 
 (** If we use propositional resizing, we can replace [f x = f y] with a proposition [R x y] in universe [a], so that the universe of [C] is the same as the universe of [A]. *)
@@ -369,5 +381,5 @@ Definition quotient_kernel_factor_small@{a a' b ab | a < a', a <= ab, b <= ab}
       IsHSet C * IsSurjection e * IsEmbedding m * (f = m o e).
 Proof.
   exact (quotient_kernel_factor_general@{a a a a' b ab ab}
-           f (fun x y => resize_hprop@{b a} (f x = f y)) (fun x y => equiv_resize_hprop _)).
+           f (fun a b => resize_hprop@{b a} (f a = f b)) (fun x y => equiv_resize_hprop _)).
 Defined.
diff --git a/theories/Modalities/Descent.v b/theories/Modalities/Descent.v
index a6c6bdba951..2bb68d9cff3 100644
--- a/theories/Modalities/Descent.v
+++ b/theories/Modalities/Descent.v
@@ -1,7 +1,7 @@
 (* -*- mode: coq; mode: visual-line -*-  *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import HFiber Extensions Limits.Pullback.
-Require Import Modality Accessible Localization.
+Require Import Modality Accessible Modalities.Localization.
 
 Local Open Scope path_scope.
 Local Open Scope subuniverse_scope.
diff --git a/theories/Modalities/Lex.v b/theories/Modalities/Lex.v
index 7ffc61cabe4..68c0c725d55 100644
--- a/theories/Modalities/Lex.v
+++ b/theories/Modalities/Lex.v
@@ -1,7 +1,7 @@
 (* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import HFiber Limits.Pullback Factorization Truncations.Core.
-Require Import Modality Accessible Localization Descent Separated.
+Require Import Modality Accessible Modalities.Localization Descent Separated.
 
 Local Open Scope path_scope.
 Local Open Scope subuniverse_scope.
diff --git a/theories/Modalities/Nullification.v b/theories/Modalities/Nullification.v
index cc037219ceb..ac6dda799fc 100644
--- a/theories/Modalities/Nullification.v
+++ b/theories/Modalities/Nullification.v
@@ -4,7 +4,7 @@
 Require Import HoTT.Basics HoTT.Types.
 Require Import Extensions.
 Require Import Modality Accessible.
-Require Export Localization.    (** Nullification is a special case of localization *)
+Require Export Modalities.Localization.    (** Nullification is a special case of localization *)
 
 Local Open Scope path_scope.