diff --git a/source/Groups/Free.lagda b/source/Groups/Free.lagda
index 5f59db0a0..09c99b5bc 100644
--- a/source/Groups/Free.lagda
+++ b/source/Groups/Free.lagda
@@ -88,8 +88,8 @@ free-groups-from-general-set-quotients
 
 \end{code}
 
-In our applications, we are interested in ℓ = id and ℓ = (_⁺) and we
-are interested in the following corollaries, which don't mention ℓ.
+We are interested in ℓ = id and ℓ = (_⁺) and we are interested in the
+following corollaries, which don't mention ℓ.
 
 The first one assumes that small set quotients exist and derives their
 effectivity from functional and propositional extensionality to get
@@ -212,7 +212,13 @@ free-groups-of-large-locally-small-types
 This means that if A is large and locally small, we can construct the
 group freely generated by A in the same universe as A, assuming only
 propositional truncations and functional and propositional
-extensionality.
+extensionality, so that additionally η is 𝓤 small, rather than 𝓤⁺
+small, which is what the above theorems give.
+
+It is this last theorem that we need, in the module Groups.Large, in
+order to prove that there is a group in 𝓤⁺ with no isomorphic copy in
+the universe 𝓤, where it is crucial that η is 𝓤 small. The 𝓤⁺
+smallness of η, given by the previous theorems, it is not enough.
 
 Organization:
 
diff --git a/source/Quotient/Type.lagda b/source/Quotient/Type.lagda
index 7029aae27..9d315dfb6 100644
--- a/source/Quotient/Type.lagda
+++ b/source/Quotient/Type.lagda
@@ -45,8 +45,8 @@ identifies-related-points (_≈_ , _) f = ∀ {x x'} → x ≈ x' → f x ＝ f
 
 To account for the module Quotient.Large, and, at the same time, usual
 (small) quotients, we introduce a parametric definion of existence of
-quotients. For small quotients we take F = id, and for large quotients
-we take F = _⁺ (see below).
+quotients. For small quotients we take ℓ = id, and for large quotients
+we take ℓ = (_⁺) (see below).
 
 \begin{code}