feat(CategoryTheory/Category/RelCat): Make rel_iso_iff universe pol…

…ymorphic. (#15854)

Make `rel_iso_iff` universe polymorphic by changing `C := Type` to `C := Type u`.

Mathlib/CategoryTheory/Category/RelCat.lean

@@ -27,7 +27,7 @@ universe u
 
 -- This file is about Lean 3 declaration "Rel".
 
-/-- A type synonym for `Type`, which carries the category instance for which
+/-- A type synonym for `Type u`, which carries the category instance for which
     morphisms are binary relations. -/
 def RelCat :=
   Type u
@@ -83,17 +83,17 @@ instance graphFunctor_essSurj : graphFunctor.EssSurj :=
     graphFunctor.essSurj_of_surj Function.surjective_id
 
 /-- A relation is an isomorphism in `RelCat` iff it is the image of an isomorphism in
-`Type`. -/
+`Type u`. -/
 theorem rel_iso_iff {X Y : RelCat} (r : X ⟶ Y) :
-    IsIso (C := RelCat) r ↔ ∃ f : (Iso (C := Type) X Y), graphFunctor.map f.hom = r := by
+    IsIso (C := RelCat) r ↔ ∃ f : (Iso (C := Type u) X Y), graphFunctor.map f.hom = r := by
   constructor
   · intro h
     have h1 := congr_fun₂ h.hom_inv_id
     have h2 := congr_fun₂ h.inv_hom_id
     simp only [RelCat.Hom.rel_comp_apply₂, RelCat.Hom.rel_id_apply₂, eq_iff_iff] at h1 h2
     obtain ⟨f, hf⟩ := Classical.axiomOfChoice (fun a => (h1 a a).mpr rfl)
     obtain ⟨g, hg⟩ := Classical.axiomOfChoice (fun a => (h2 a a).mpr rfl)
-    suffices hif : IsIso (C := Type) f by
+    suffices hif : IsIso (C := Type u) f by
       use asIso f
       ext x y
       simp only [asIso_hom, graphFunctor_map]