diff --git a/STYLE.md b/STYLE.md
index f0b0b3c15a5..72ca480201d 100644
--- a/STYLE.md
+++ b/STYLE.md
@@ -339,6 +339,11 @@ The inverse function can then be referred to as `foo ^-1`.  Avoid
 using `equiv_foo` unless you really do need an `Equiv` object, rather
 than a function which happens to be an equivalence.
 
+On the other hand, sometimes it is easier to define an equivalence
+by composing together existing equivalences, in which case one goes
+immediately to the last step, defining `equiv_foo`.  If the equivalence
+is used frequently as an ordinary function, one might also define `foo`
+as the underlying function of `equiv_foo`; see `path_equiv`, as an example.
 
 ## 3. Records, Structures, Typeclasses ##
 
diff --git a/theories/Algebra/Groups/QuotientGroup.v b/theories/Algebra/Groups/QuotientGroup.v
index 91c0c3396f1..765ae89a41c 100644
--- a/theories/Algebra/Groups/QuotientGroup.v
+++ b/theories/Algebra/Groups/QuotientGroup.v
@@ -30,9 +30,8 @@ Section GroupCongruenceQuotient.
     srapply Quotient_rec2.
     - intros x y.
       exact (class_of _ (x * y)).
-    - intros x x' p y y' q.
-      apply qglue.
-      by apply iscong.
+    - intros x x' y p. apply qglue. by apply iscong.
+    - intros x y y' q. apply qglue. by apply iscong.
   Defined.
 
   Global Instance congquot_mon_unit : MonUnit CongruenceQuotient.
diff --git a/theories/Algebra/Rings/Localization.v b/theories/Algebra/Rings/Localization.v
index 2e5197ca3a7..db5873a094f 100644
--- a/theories/Algebra/Rings/Localization.v
+++ b/theories/Algebra/Rings/Localization.v
@@ -166,13 +166,11 @@ Section Localization.
   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.
+    - intros f1 f1' f2 p.  by apply qglue, frac_add_wd_l.
+    - intros f1 f2 f2' q.  by apply qglue, frac_add_wd_r.
   Defined.
 
   (** *** Multiplication operation *)
@@ -212,15 +210,13 @@ Section Localization.
   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.
+    - intros f1 f1' f2 p; cbn beta.
+      by apply qglue, frac_mult_wd_l.
+    - intros f1 f2 f2' q; cbn beta.
+      by apply qglue, frac_mult_wd_r.
   Defined.
 
   (** *** Zero element *)
diff --git a/theories/Algebra/Rings/QuotientRing.v b/theories/Algebra/Rings/QuotientRing.v
index 514c3a1a99f..f191421ea13 100644
--- a/theories/Algebra/Rings/QuotientRing.v
+++ b/theories/Algebra/Rings/QuotientRing.v
@@ -42,9 +42,8 @@ Section QuotientRing.
   Proof.
     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 x x' y p. apply qglue. by apply iscong.
+    - intros x y y' q. apply qglue. by apply iscong.
   Defined.
 
   Instance one_quotient_abgroup : One (QuotientAbGroup R I) := class_of _ one.
diff --git a/theories/Basics/Overture.v b/theories/Basics/Overture.v
index 779cda59d5e..b627e05404b 100644
--- a/theories/Basics/Overture.v
+++ b/theories/Basics/Overture.v
@@ -655,10 +655,9 @@ Existing Class Funext.
 Axiom isequiv_apD10 : forall `{Funext} (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g).
 Global Existing Instance isequiv_apD10.
 
-Definition path_forall `{Funext} {A : Type} {P : A -> Type} (f g : forall x : A, P x) :
-  f == g -> f = g
-  :=
-  (@apD10 A P f g)^-1.
+Definition path_forall `{Funext} {A : Type} {P : A -> Type} (f g : forall x : A, P x)
+  : f == g -> f = g
+  := (@apD10 A P f g)^-1.
 
 Global Arguments path_forall {_ A%_type_scope P} (f g)%_function_scope _.
 
@@ -674,9 +673,6 @@ Global Arguments path_forall {_ A%_type_scope P} (f g)%_function_scope _.
 #[export] Hint Resolve idpath inverse : path_hints.
 #[export] Hint Resolve idpath : core.
 
-Ltac path_via mid :=
-  apply @concat with (y := mid); auto with path_hints.
-
 (** ** Natural numbers *)
 
 (**  Natural numbers. *)
@@ -688,13 +684,6 @@ Scheme nat_ind := Induction for nat Sort Type.
 Scheme nat_rect := Induction for nat Sort Type.
 Scheme nat_rec := Induction for nat Sort Type.
 
-(** These schemes are therefore defined in Spaces.Nat *)
-(*
-Scheme nat_ind := Induction for nat Sort Type.
-Scheme nat_rect := Induction for nat Sort Type.
-Scheme nat_rec := Minimality for nat Sort Type.
- *)
-
 Declare Scope nat_scope.
 Delimit Scope nat_scope with nat.
 Bind Scope nat_scope with nat.
diff --git a/theories/Basics/Tactics.v b/theories/Basics/Tactics.v
index 9cc6200b67a..c8e24b779a6 100644
--- a/theories/Basics/Tactics.v
+++ b/theories/Basics/Tactics.v
@@ -6,6 +6,10 @@ Require Import Basics.Overture.
 
 (** This module implements various tactics used in the library. *)
 
+(** If the goal is [x = z], [path_via y] will replace this with two goals, [x = y] and [y = z]. *)
+Ltac path_via mid :=
+  apply @concat with (y := mid); auto with path_hints.
+
 (** The following tactic is designed to be more or less interchangeable with [induction n as [ | n' IH ]] whenever [n] is a [nat] or a [trunc_index].  The difference is that it produces proof terms involving [fix] explicitly rather than [nat_ind] or [trunc_index_ind], and therefore does not introduce higher universe parameters. It works if [n] is in the context or in the goal. *)
 Ltac simple_induction n n' IH :=
   try generalize dependent n;
diff --git a/theories/Colimits/Quotient.v b/theories/Colimits/Quotient.v
index 3ee2c9cb201..feae531e280 100644
--- a/theories/Colimits/Quotient.v
+++ b/theories/Colimits/Quotient.v
@@ -8,7 +8,7 @@ Require Import PropResizing.
 
 Local Open Scope path_scope.
 
-(** * The set-quotient of a type by an hprop-valued relation
+(** * The set-quotient of a type by a relation
 
 We aim to model:
 <<
@@ -19,7 +19,10 @@ Inductive Quotient R : Type :=
 >>
 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]. *)
+Some results require additional assumptions, for example, that the relation be hprop-valued, or that the relation be reflexive, transitive or symmetric.
+
+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).
@@ -92,7 +95,7 @@ Arguments Quotient_rec_beta_qglue : simpl never.
 
 Notation "A / R" := (Quotient (A:=A) R).
 
-(* Quotient induction into a hprop. *)
+(** Quotient induction into an 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))
@@ -122,12 +125,51 @@ Proof.
   exact (dclass a b c).
 Defined.
 
+Definition Quotient_ind2 {A : Type} (R : Relation A)
+  (P : A / R -> A / R -> Type) `{forall x y, IsHSet (P x y)}
+  (dclass : forall a b, P (class_of R a) (class_of R b))
+  (dequiv_l : forall a a' b (p : R a a'),
+    transport (fun x => P x _) (qglue p) (dclass a b) = dclass a' b)
+  (dequiv_r : forall a b b' (p : R b b'), qglue p # dclass a b = dclass a b')
+  : forall x y, P x y.
+Proof.
+  intro x.
+  srapply Quotient_ind.
+  - intro b.
+    revert x.
+    srapply Quotient_ind.
+    + intro a.
+      exact (dclass a b).
+    + cbn beta.
+      intros a a' p.
+      by apply dequiv_l.
+  - cbn beta.
+    intros b b' p.
+    revert x.
+    srapply Quotient_ind_hprop; simpl.
+    intro a; by apply dequiv_r.
+Defined.
+
+Definition Quotient_rec2 {A : Type} (R : Relation A) (B : Type) `{IsHSet B}
+  (dclass : A -> A -> B)
+  (dequiv_l : forall a a' b, R a a' -> dclass a b = dclass a' b)
+  (dequiv_r : forall a b b', R b b' -> dclass a b = dclass a b')
+  : A / R -> A / R -> B.
+Proof.
+  srapply Quotient_ind2.
+  - exact dclass.
+  - intros; lhs nrapply transport_const.
+    by apply dequiv_l.
+  - intros; lhs nrapply transport_const.
+    by apply dequiv_r.
+Defined.
+
 Section Equiv.
 
   Context `{Univalence} {A : Type} (R : Relation A) `{is_mere_relation _ R}
     `{Transitive _ R} `{Symmetric _ R} `{Reflexive _ R}.
 
-  (* The proposition of being in a given class in a quotient. *)
+  (** The proposition of being in a given class in a quotient. This requires [Univalence] so that we know that [HProp] is a set. *)
   Definition in_class : A / R -> A -> HProp.
   Proof.
     intros x b; revert x.
@@ -140,20 +182,20 @@ Section Equiv.
     apply (transitivity p).
   Defined.
 
-  (* Being in a class is decidable if the Relation is decidable. *)
+  (** Being in a class is decidable if the relation is decidable. *)
   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. *)
+  (** If [a] is in a class [x], then the class of [a] is equal to [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.
+    { intros a b p.
       exact (qglue p). }
-    intros x y p.
+    intros a b p.
     funext ? ?.
     apply hset_path2.
   Defined.
@@ -167,7 +209,7 @@ Section Equiv.
     cbv; reflexivity.
   Defined.
 
-  (** Thm 10.1.8 *)
+  (** Theorem 10.1.8. *)
   Theorem path_quotient (a b : A)
     : R a b <~> (class_of R a = class_of R b).
   Proof.
@@ -176,33 +218,7 @@ Section Equiv.
     - apply related_quotient_paths.
   Defined.
 
-  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 b.
-      revert x.
-      srapply Quotient_rec.
-      + 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. *)
+  (** The map [class_of : A -> A/R] is a surjection. *)
   Global Instance issurj_class_of : IsSurjection (class_of R).
   Proof.
     apply BuildIsSurjection.
@@ -212,8 +228,7 @@ Section Equiv.
     by exists a.
   Defined.
 
-  (* Universal property of quotient *)
-  (* Lemma 6.10.3 *)
+  (** The universal property of the quotient.  This is Lemma 6.10.3. *)
   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.
diff --git a/theories/Diagrams/CommutativeSquares.v b/theories/Diagrams/CommutativeSquares.v
index de7daa11976..01cceb906e3 100644
--- a/theories/Diagrams/CommutativeSquares.v
+++ b/theories/Diagrams/CommutativeSquares.v
@@ -1,4 +1,4 @@
-Require Import Basics.Overture Basics.PathGroupoids.
+Require Import Basics.Overture Basics.PathGroupoids Basics.Tactics.
 
 (** * Comutative squares *)