chore: better TypeMax instances for limits in Type (#5535)

Preliminary to the full forward port of leanprover-community/mathlib#19153, 
this is a slight generalization along with explanation of the problem with the instances.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Mathlib/CategoryTheory/Limits/Shapes/Types.lean

@@ -38,30 +38,56 @@ We first construct terms of `IsLimit` and `LimitCone`, and then provide isomorph
 types generated by the `HasLimit` API.
 
 As an example, when setting up the monoidal category structure on `Type`
-we use the `types_has_terminal` and `types_has_binary_products` instances.
+we use the `Types.terminalLimitCone` and `Types.binaryProductLimitCone` definitions.
 -/
 
 
-universe u v
+universe v u
 
 open CategoryTheory Limits
 
 namespace CategoryTheory.Limits.Types
 
+instance {β : Type v} (f : β → TypeMax.{v, u}) : HasProduct f :=
+HasLimitsOfShape.has_limit (Discrete.functor f)
+
+-- This must have higher priority than the instance for `TypeMax`.
+-- (Merely being defined later is enough, but that is fragile.)
+instance (priority := high) {β : Type v} (f : β → Type v) : HasProduct f :=
+HasLimitsOfShape.has_limit (Discrete.functor f)
+
 /-- A restatement of `Types.Limit.lift_π_apply` that uses `Pi.π` and `Pi.lift`. -/
 @[simp 1001]
-theorem pi_lift_π_apply {β : Type u} (f : β → Type u) {P : Type u} (s : ∀ b, P ⟶ f b) (b : β)
-    (x : P) : (Pi.π f b : (∏ f) → f b) (@Pi.lift β _ _ f _ P s x) = s b x :=
+theorem pi_lift_π_apply {β : Type v} (f : β → TypeMax.{v, u}) {P : TypeMax.{v, u}}
+    (s : ∀ b, P ⟶ f b) (b : β) (x : P) :
+    (Pi.π f b : (piObj f) → f b) (@Pi.lift β _ _ f _ P s x) = s b x :=
   congr_fun (limit.lift_π (Fan.mk P s) ⟨b⟩) x
 #align category_theory.limits.types.pi_lift_π_apply CategoryTheory.Limits.Types.pi_lift_π_apply
 
+/-- A restatement of `Types.Limit.lift_π_apply` that uses `Pi.π` and `Pi.lift`,
+with specialized universes. -/
+@[simp 1001]
+theorem pi_lift_π_apply' {β : Type v} (f : β → Type v) {P : Type v}
+    (s : ∀ b, P ⟶ f b) (b : β) (x : P) :
+    (Pi.π f b : (piObj f) → f b) (@Pi.lift β _ _ f _ P s x) = s b x :=
+  congr_fun (limit.lift_π (Fan.mk P s) ⟨b⟩) x
+#align category_theory.limits.types.pi_lift_π_apply' CategoryTheory.Limits.Types.pi_lift_π_apply'
+
 /-- A restatement of `Types.Limit.map_π_apply` that uses `Pi.π` and `Pi.map`. -/
 @[simp 1001]
-theorem pi_map_π_apply {β : Type u} {f g : β → Type u} (α : ∀ j, f j ⟶ g j) (b : β) (x) :
+theorem pi_map_π_apply {β : Type v} {f g : β → TypeMax.{v, u}} (α : ∀ j, f j ⟶ g j) (b : β) (x) :
     (Pi.π g b : (∏ g) → g b) (Pi.map α x) = α b ((Pi.π f b : (∏ f) → f b) x) :=
-  Limit.map_π_apply' _ _ _
+  Limit.map_π_apply _ _ _
 #align category_theory.limits.types.pi_map_π_apply CategoryTheory.Limits.Types.pi_map_π_apply
 
+/-- A restatement of `Types.Limit.map_π_apply` that uses `Pi.π` and `Pi.map`,
+with specialized universes. -/
+@[simp 1001]
+theorem pi_map_π_apply' {β : Type v} {f g : β → Type v} (α : ∀ j, f j ⟶ g j) (b : β) (x) :
+    (Pi.π g b : (∏ g) → g b) (Pi.map α x) = α b ((Pi.π f b : (∏ f) → f b) x) :=
+  Limit.map_π_apply' _ _ _
+#align category_theory.limits.types.pi_map_π_apply' CategoryTheory.Limits.Types.pi_map_π_apply'
+
 /-- The category of types has `PUnit` as a terminal object. -/
 def terminalLimitCone : Limits.LimitCone (Functor.empty (Type u)) where
   -- porting note: tidy was able to fill the structure automatically
@@ -315,7 +341,7 @@ noncomputable def isCoprodOfMono {X Y : Type u} (f : X ⟶ Y) [Mono f] :
 
 /-- The category of types has `Π j, f j` as the product of a type family `f : J → Type`.
 -/
-def productLimitCone {J : Type u} (F : J → TypeMax.{u, v}) :
+def productLimitCone {J : Type v} (F : J → TypeMax.{v, u}) :
     Limits.LimitCone (Discrete.functor F) where
   cone :=
     { pt := ∀ j, F j
@@ -326,21 +352,21 @@ def productLimitCone {J : Type u} (F : J → TypeMax.{u, v}) :
 #align category_theory.limits.types.product_limit_cone CategoryTheory.Limits.Types.productLimitCone
 
 /-- The categorical product in `Type u` is the type theoretic product `Π j, F j`. -/
-noncomputable def productIso {J : Type u} (F : J → TypeMax.{u, v}) : ∏ F ≅ ∀ j, F j :=
-  limit.isoLimitCone (productLimitCone.{u, v} F)
+noncomputable def productIso {J : Type v} (F : J → TypeMax.{v, u}) : ∏ F ≅ ∀ j, F j :=
+  limit.isoLimitCone (productLimitCone.{v, u} F)
 #align category_theory.limits.types.product_iso CategoryTheory.Limits.Types.productIso
 
 -- porting note: was `@[elementwise (attr := simp)]`, but it produces a trivial lemma.
 @[simp]
-theorem productIso_hom_comp_eval {J : Type u} (F : J → TypeMax.{u, v}) (j : J) :
-    ((productIso.{u, v} F).hom ≫ fun f => f j) = Pi.π F j :=
+theorem productIso_hom_comp_eval {J : Type v} (F : J → TypeMax.{v, u}) (j : J) :
+    ((productIso.{v, u} F).hom ≫ fun f => f j) = Pi.π F j :=
   rfl
 #align category_theory.limits.types.product_iso_hom_comp_eval CategoryTheory.Limits.Types.productIso_hom_comp_eval
 
 @[elementwise (attr := simp)]
-theorem productIso_inv_comp_π {J : Type u} (F : J → TypeMax.{u, v}) (j : J) :
-    (productIso.{u, v} F).inv ≫ Pi.π F j = fun f => f j :=
-  limit.isoLimitCone_inv_π (productLimitCone.{u, v} F) ⟨j⟩
+theorem productIso_inv_comp_π {J : Type v} (F : J → TypeMax.{v, u}) (j : J) :
+    (productIso.{v, u} F).inv ≫ Pi.π F j = fun f => f j :=
+  limit.isoLimitCone_inv_π (productLimitCone.{v, u} F) ⟨j⟩
 #align category_theory.limits.types.product_iso_inv_comp_π CategoryTheory.Limits.Types.productIso_inv_comp_π
 
 /-- The category of types has `Σ j, f j` as the coproduct of a type family `f : J → Type`.

Mathlib/CategoryTheory/Limits/Types.lean

@@ -80,6 +80,30 @@ instance hasLimit (F : J ⥤ TypeMax.{v, u}) : HasLimit F :=
 instance hasLimit' (F : J ⥤ Type v) : HasLimit F :=
   hasLimit.{v, v} F
 
+-- This instance is not necessary, and indeed unhelpful:
+-- if it has higher priority than the instance for `TypeMax.{w, v}`,
+-- or has the same priority and is defined later,
+-- then it blocks successful typeclass search with universe unification errors.
+instance : HasLimitsOfSize.{w, w, max v w, max (v + 1) (w + 1)} (Type max v w) :=
+  Types.hasLimitsOfSize.{w, v}
+
+-- This either needs to have higher priority (safer) or come after the instance for `Type max v w`.
+instance (priority := 1100) :
+    HasLimitsOfSize.{w, w, max v w, max (v + 1) (w + 1)} (TypeMax.{w, v}) :=
+  Types.hasLimitsOfSize.{w, v}
+
+-- This needs to have priority higher than the instance for `TypeMax.{w, v}`.
+instance (priority := 1200) : HasLimitsOfSize.{v, v, v, v + 1} (Type v) :=
+  Types.hasLimitsOfSize.{v, v}
+
+-- Verify that we can find instances, at least when we ask for `TypeMax.{w, v}`:
+example : HasLimitsOfSize.{w, w, max v w, max (v + 1) (w + 1)} (TypeMax.{w, v}) := inferInstance
+example : HasLimitsOfSize.{0, 0, v, v+1} (Type v) := inferInstance
+example : HasLimitsOfSize.{v, v, v, v+1} (Type v) := inferInstance
+-- Note however this fails unless we modify the universe unification algorithm:
+-- `stuck at solving universe constraint max (v+1) (w+1) =?= max (w+1) (?u+1)`
+-- example : HasLimitsOfSize.{w, w, max v w, max (v + 1) (w + 1)} (Type max v w) := inferInstance
+
 /-- The equivalence between a limiting cone of `F` in `Type u` and the "concrete" definition as the
 sections of `F`.
 -/

Mathlib/Topology/Sheaves/SheafCondition/UniqueGluing.lean

@@ -118,9 +118,9 @@ theorem compatible_iff_leftRes_eq_rightRes (sf : piOpens F U) :
     exact h i j
   · intro i j
     convert congr_arg (Limits.Pi.π (fun p : ι × ι => F.obj (op (U p.1 ⊓ U p.2))) (i, j)) h
-    · rw [leftRes, Types.pi_lift_π_apply]
+    · rw [leftRes, Types.pi_lift_π_apply']
       rfl
-    · rw [rightRes, Types.pi_lift_π_apply]
+    · rw [rightRes, Types.pi_lift_π_apply']
       rfl
 set_option linter.uppercaseLean3 false in
 #align Top.presheaf.compatible_iff_left_res_eq_right_res TopCat.Presheaf.compatible_iff_leftRes_eq_rightRes
@@ -139,7 +139,7 @@ theorem isGluing_iff_eq_res (sf : piOpens F U) (s : F.obj (op (iSup U))) :
     exact h i
   · intro i
     convert congr_arg (Limits.Pi.π (fun i : ι => F.obj (op (U i))) i) h
-    rw [res, Types.pi_lift_π_apply]
+    rw [res, Types.pi_lift_π_apply']
     rfl
 set_option linter.uppercaseLean3 false in
 #align Top.presheaf.is_gluing_iff_eq_res TopCat.Presheaf.isGluing_iff_eq_res