re-fix

src/Init/Core.lean

@@ -1908,11 +1908,11 @@ instance Pi.instSubsingleton {α : Sort u} {β : α → Sort v} [∀ a, Subsingl
 
 /-! # Squash -/
 
-theorem true_equivalence : @Equivalence α fun _ _ ↦ True :=
+theorem true_equivalence (α : Sort u) : Equivalence fun _ _ : α ↦ True :=
   ⟨fun _ ↦ trivial, fun _ ↦ trivial, fun _ _ ↦ trivial⟩
 
 /-- Always-true relation as a `Setoid`. -/
-def trueSetoid : Setoid α :=
+def trueSetoid (α : Sort u) : Setoid α :=
   ⟨_, true_equivalence⟩
 
 /--
@@ -1929,7 +1929,7 @@ 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.
 -/
-def Squash (α : Sort u) := @Quotient α trueSetoid
+def Squash (α : Sort u) := Quotient (trueSetoid α)
 
 /-- The canonical quotient map into `Squash α`. -/
 def Squash.mk {α : Sort u} (x : α) : Squash α := Quot.mk _ x