chore(Logic): generalise universes for relator and relation (leanprover-community#34391)

The definitions from core are already in `Sort`, so it makes sense for the mathlib lemmas about them to work here too.

Author: b-mehta

Mathlib/Logic/Relation.lean

@@ -52,7 +52,7 @@ the bundled version, see `Rel`.
 
 open Function
 
-variable {α β γ δ ε ζ : Type*}
+variable {α β γ δ ε ζ : Sort*}
 
 section NeImp
 

Mathlib/Logic/Relator.lean

@@ -41,7 +41,7 @@ end
 
 section
 
-variable {α : Type u₁} {β : Type u₂} (R : α → β → Prop)
+variable {α : Sort u₁} {β : Sort u₂} (R : α → β → Prop)
 
 /-- A relation is "right total" if every element appears on the right. -/
 def RightTotal : Prop := ∀ b, ∃ a, R a b