quotient.patch

diff --git a/theories/Classes/implementations/field_of_fractions.v b/theories/Classes/implementations/field_of_fractions.v
index 853f5f748..015b3e17a 100644
--- a/theories/Classes/implementations/field_of_fractions.v
+++ b/theories/Classes/implementations/field_of_fractions.v
@@ -301,12 +301,13 @@ Definition F_rec_compute T sT dclass dequiv x
   : @F_rec T sT dclass dequiv (' x) = dclass x
   := 1.
 
-Definition F_rec2@{i j} {T:Type@{i} } {sT : IsHSet T}
+Definition F_rec2@{i} {T:Type@{i} } {sT : IsHSet T}
   : forall (dclass : Frac R -> Frac R -> T)
   (dequiv : forall x1 x2, equiv x1 x2 -> forall y1 y2, equiv y1 y2 ->
     dclass x1 y1 = dclass x2 y2),
   F -> F -> T
-  := @quotient_rec2@{UR UR j i} _ _ _ _ _ (Build_HSet _).
+  := @quotient_rec2@{UR UR UR} _ _ _ _ _ (Build_HSet _).
+(* This now requires i <= UR, which may not be intended. *)
 
 Definition F_rec2_compute {T sT} dclass dequiv x y
   : @F_rec2 T sT dclass dequiv (' x) (' y) = dclass x y
@@ -405,7 +406,7 @@ Defined.
 
 Lemma classes_eq_related@{} : forall q r, ' q = ' r -> equiv q r.
 Proof.
-apply classes_eq_related@{UR UR Ularge Uhuge};apply _.
+apply classes_eq_related@{UR Ularge};apply _.
 Qed.
 
 Lemma class_neq@{} : forall q r, ~ (equiv q r) -> ' q <> ' r.
diff --git a/theories/Classes/implementations/natpair_integers.v b/theories/Classes/implementations/natpair_integers.v
index d8389f724..84175e930 100644
--- a/theories/Classes/implementations/natpair_integers.v
+++ b/theories/Classes/implementations/natpair_integers.v
@@ -321,7 +321,7 @@ Definition Z_path {x y} : PairT.equiv x y -> Z_of_pair x = Z_of_pair y
   := related_classes_eq _.
 
 Definition related_path {x y} : Z_of_pair x = Z_of_pair y -> PairT.equiv x y
-  := classes_eq_related@{UN UN Ularge Uhuge} _ _ _.
+  := classes_eq_related@{UN Ularge} _ _ _.
 
 Definition Z_rect@{i} (P : Z -> Type@{i}) {sP : forall x, IsHSet (P x)}
   (dclass : forall x : PairT.T N, P (' x))
@@ -372,12 +372,12 @@ Definition Z_rec_compute T sT dclass dequiv x
   : @Z_rec T sT dclass dequiv (' x) = dclass x
   := 1.
 
-Definition Z_rec2@{i j} {T:Type@{i} } {sT : IsHSet T}
+Definition Z_rec2@{i} {T:Type@{i} } {sT : IsHSet T}
   : forall (dclass : PairT.T N -> PairT.T N -> T)
   (dequiv : forall x1 x2, PairT.equiv x1 x2 -> forall y1 y2, PairT.equiv y1 y2 ->
     dclass x1 y1 = dclass x2 y2),
   Z -> Z -> T
-  := @quotient_rec2@{UN UN j i} _ _ _ _ _ (Build_HSet _).
+  := @quotient_rec2@{UN UN UN} _ _ _ _ _ (Build_HSet _).
 
 Definition Z_rec2_compute {T sT} dclass dequiv x y
   : @Z_rec2 T sT dclass dequiv (' x) (' y) = dclass x y
@@ -498,8 +498,9 @@ Qed.
 
 Definition Zle_HProp@{} : Z -> Z -> HProp@{UN}.
 Proof.
-apply (@Z_rec2@{Ularge Ularge} _ (@trunctype_istrunc@{Ularge} _ _)
+apply (@Z_rec2@{Ularge} _ (@trunctype_istrunc@{Ularge} _ _)
   (fun q r => Build_HProp (PairT.Tle q r))).
+(* Coq doesn't accept the above. *)
 intros. apply path_hprop. simpl.
 apply (PairT.le_respects _);trivial.
 Defined.
diff --git a/theories/HIT/quotient.v b/theories/HIT/quotient.v
index 229ad25ec..37f288ed7 100644
--- a/theories/HIT/quotient.v
+++ b/theories/HIT/quotient.v
@@ -22,7 +22,9 @@ Module Export Quotient.
 
   Section Domain.
 
-    Context {A : Type} (R : Relation A) {sR: is_mere_relation _ R}.
+    Universe u.
+
+    Context {A : Type@{u}} (R : Relation@{u u} A) {sR: is_mere_relation _ R}.
 
     (** We choose to let the definition of quotient depend on the proof that [R] is a set-relations.  Alternatively, we could have defined it for all relations and only develop the theory for set-relations.  The former seems more natural.
 
@@ -32,7 +34,7 @@ We do not require [R] to be an equivalence relation, but implicitly consider its
     (** Note: If we wanted to be really accurate, we'd need to put [@quotient A R sr] in the max [U_{sup(i, j)}] of the universes of [A : U_i] and [R : A -> A -> U_j].  But this requires some hacky code, at the moment, and the only thing we gain is avoiding making use of an implicit hpropositional resizing "axiom". *)
 
     (** This definition has a parameter [sR] that shadows the ambient one in the Context in order to ensure that it actually ends up depending on everything in the Context when the section is closed, since its definition doesn't actually refer to any of them.  *)
-    Private Inductive quotient {sR: is_mere_relation _ R} : Type :=
+    Private Inductive quotient {sR: is_mere_relation _ R} : Type@{u} :=
     | class_of : A -> quotient.
 
     (** The path constructors. *)
@@ -68,9 +70,11 @@ End Quotient.
 
 Section Equiv.
 
+  Universe u.
+
   Context `{Univalence}.
 
-  Context {A : Type} (R : Relation A) {sR: is_mere_relation _ R}
+  Context {A : Type@{u}} (R : Relation@{u u} A) {sR: is_mere_relation _ R}
           {Htrans : Transitive R} {Hsymm : Symmetric R}.
 
   Lemma quotient_path2 : forall {x y : quotient R} (p q : x=y), p=q.