feat: define Squash as a Quotient

src/Init/Core.lean

@@ -1908,6 +1908,13 @@ instance Pi.instSubsingleton {α : Sort u} {β : α → Sort v} [∀ a, Subsingl
 
 /-! # Squash -/
 
+theorem equivalence_true (α : Sort u) : Equivalence fun _ _ : α ↦ True :=
+  ⟨fun _ ↦ trivial, fun _ ↦ trivial, fun _ _ ↦ trivial⟩
+
+/-- Always-true relation as a `Setoid`. -/
+def Setoid.trivial (α : Sort u) : Setoid α :=
+  ⟨_, equivalence_true α⟩
+
 /--
 `Squash α` is the quotient of `α` by the always true relation.
 It is empty if `α` is empty, otherwise it is a singleton.
@@ -1921,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) := Quot (fun (_ _ : α) => True)
+def Squash (α : Sort u) := Quotient (Setoid.trivial α)
 
 /-- The canonical quotient map into `Squash α`. -/
 def Squash.mk {α : Sort u} (x : α) : Squash α := Quot.mk _ x