add doc comment

src/Init/Core.lean

@@ -1908,12 +1908,12 @@ instance Pi.instSubsingleton {α : Sort u} {β : α → Sort v} [∀ a, Subsingl
 
 /-! # Squash -/
 
-theorem true_equivalence (α : Sort u) : Equivalence fun _ _ : α ↦ True :=
+theorem equivalence_true (α : Sort u) : Equivalence fun _ _ : α ↦ True :=
   ⟨fun _ ↦ trivial, fun _ ↦ trivial, fun _ _ ↦ trivial⟩
 
 /-- Always-true relation as a `Setoid`. -/
-def trueSetoid (α : Sort u) : Setoid α :=
-  ⟨_, true_equivalence α⟩
+def Setoid.trivial (α : Sort u) : Setoid α :=
+  ⟨_, equivalence_true α⟩
 
 /--
 `Squash α` is the quotient of `α` by the always true relation.
@@ -1928,8 +1928,12 @@ represents an element of `Squash α` the same as `α` itself
 
 `Squash.lift` will extract a value in any subsingleton `β` from a function on `α`,
 while `Nonempty.rec` can only do the same when `β` is a proposition.
+
+We define `Squash` in terms of `Quotient` rather than just `Quot`. This means that
+`Squash` can be used when a `Quotient` argument is expected, and the setoid will be
+automatically inferred.
 -/
-def Squash (α : Sort u) := Quotient (trueSetoid α)
+def Squash (α : Sort u) := Quotient (Setoid.trivial α)
 
 /-- The canonical quotient map into `Squash α`. -/
 def Squash.mk {α : Sort u} (x : α) : Squash α := Quot.mk _ x