feat: using UnivLE in constructing limits in Type (#5724)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Apurva <apurvnakade@gmail.com>
Co-authored-by: Jon Eugster <eugster.jon@gmail.com>
Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
Co-authored-by: Johan Commelin <johan@commelin.net>

Mathlib/Algebra/Category/GroupCat/Limits.lean

@@ -67,7 +67,7 @@ set_option linter.uppercaseLean3 false in
 #align AddGroup.sections_add_subgroup AddGroupCat.sectionsAddSubgroup
 
 @[to_additive]
-instance limitGroup (F : J ⥤ GroupCatMax.{v, u}) :
+noncomputable instance limitGroup (F : J ⥤ GroupCatMax.{v, u}) :
     Group (Types.limitCone.{v, u} (F ⋙ forget GroupCat)).pt := by
   change Group (sectionsSubgroup.{v, u} F)
   infer_instance

Mathlib/Algebra/Category/MonCat/Limits.lean

@@ -72,7 +72,7 @@ instance limitMonoid (F : J ⥤ MonCatMax.{u,v}) :
 
 /-- `limit.π (F ⋙ forget MonCat) j` as a `MonoidHom`. -/
 @[to_additive "`limit.π (F ⋙ forget AddMonCat) j` as an `AddMonoidHom`."]
-def limitπMonoidHom (F : J ⥤ MonCatMax.{u, v}) (j : J) :
+noncomputable def limitπMonoidHom (F : J ⥤ MonCatMax.{u, v}) (j : J) :
   (Types.limitCone.{v, u} (F ⋙ forget MonCatMax.{u, v})).pt →*
     ((F ⋙ forget MonCat.{max v u}).obj j) :=
   { toFun := (Types.limitCone.{v, u} (F ⋙ forget MonCatMax.{u, v})).π.app j,
@@ -90,7 +90,7 @@ namespace HasLimits
 (Internal use only; use the limits API.)
 -/
 @[to_additive "(Internal use only; use the limits API.)"]
-def limitCone (F : J ⥤ MonCatMax.{u,v}) : Cone F :=
+noncomputable def limitCone (F : J ⥤ MonCatMax.{u,v}) : Cone F :=
   { pt := MonCat.of (Types.limitCone (F ⋙ forget _)).pt
     π :=
     { app := limitπMonoidHom F
@@ -104,7 +104,7 @@ def limitCone (F : J ⥤ MonCatMax.{u,v}) : Cone F :=
 (Internal use only; use the limits API.)
 -/
 @[to_additive "(Internal use only; use the limits API.)"]
-def limitConeIsLimit (F : J ⥤ MonCatMax.{u,v}) : IsLimit (limitCone F) := by
+noncomputable def limitConeIsLimit (F : J ⥤ MonCatMax.{u,v}) : IsLimit (limitCone F) := by
   refine IsLimit.ofFaithful (forget MonCatMax) (Types.limitConeIsLimit.{v,u} _)
     (fun s => ⟨⟨_, ?_⟩, ?_⟩) (fun s => rfl) <;>
   aesop_cat
@@ -137,7 +137,8 @@ instance hasLimits : HasLimits MonCat.{u} :=
 This means the underlying type of a limit can be computed as a limit in the category of types. -/
 @[to_additive "The forgetful functor from additive monoids to types preserves all limits.\n\n
 This means the underlying type of a limit can be computed as a limit in the category of types."]
-instance forgetPreservesLimitsOfSize : PreservesLimitsOfSize.{v} (forget MonCatMax.{u,v}) where
+noncomputable instance forgetPreservesLimitsOfSize :
+    PreservesLimitsOfSize.{v} (forget MonCatMax.{u,v}) where
   preservesLimitsOfShape {_} _ :=
     { preservesLimit := fun {F} =>
         preservesLimitOfPreservesLimitCone (limitConeIsLimit F)
@@ -146,7 +147,7 @@ instance forgetPreservesLimitsOfSize : PreservesLimitsOfSize.{v} (forget MonCatM
 #align AddMon.forget_preserves_limits_of_size AddMonCat.forgetPreservesLimitsOfSize
 
 @[to_additive]
-instance forgetPreservesLimits : PreservesLimits (forget MonCat.{u}) :=
+noncomputable instance forgetPreservesLimits : PreservesLimits (forget MonCat.{u}) :=
   MonCat.forgetPreservesLimitsOfSize.{u, u}
 #align Mon.forget_preserves_limits MonCat.forgetPreservesLimits
 #align AddMon.forget_preserves_limits AddMonCat.forgetPreservesLimits

Mathlib/CategoryTheory/Closed/Types.lean

@@ -43,6 +43,7 @@ instance (X : Type v₁) : IsLeftAdjoint (Types.binaryProductFunctor.obj X) wher
       { unit := { app := fun Z (z : Z) x => ⟨x, z⟩ }
         counit := { app := fun Z xf => xf.2 xf.1 } }
 
+-- Porting note: this instance should be moved to a higher file.
 instance : HasFiniteProducts (Type v₁) :=
   hasFiniteProducts_of_hasProducts.{v₁} _
 

Mathlib/CategoryTheory/Limits/Shapes/Types.lean

@@ -48,44 +48,42 @@ open CategoryTheory Limits
 
 namespace CategoryTheory.Limits.Types
 
-instance {β : Type v} (f : β → TypeMax.{v, u}) : HasProduct f :=
-HasLimitsOfShape.has_limit (Discrete.functor f)
+example : HasProducts.{v} (Type v) := inferInstance
+example [UnivLE.{v, u}] : HasProducts.{v} (Type u) := inferInstance
 
--- 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)
+-- This shortcut instance is required in `Mathlib.CategoryTheory.Closed.Types`,
+-- although I don't understand why, and wish it wasn't.
+instance : HasProducts.{v} (Type v) := inferInstance
 
 /-- A restatement of `Types.Limit.lift_π_apply` that uses `Pi.π` and `Pi.lift`. -/
 @[simp 1001]
-theorem pi_lift_π_apply {β : Type v} (f : β → TypeMax.{v, u}) {P : TypeMax.{v, u}}
+theorem pi_lift_π_apply [UnivLE.{v, u}] {β : Type v} (f : β → Type u) {P : Type 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
+  by simp
 #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 v} {f g : β → TypeMax.{v, u}} (α : ∀ j, f j ⟶ g j) (b : β) (x) :
+theorem pi_map_π_apply [UnivLE.{v, u}] {β : Type v} {f g : β → Type 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.{v, u} _ _ _
 #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' _ _ _
+   by simp
 #align category_theory.limits.types.pi_map_π_apply' CategoryTheory.Limits.Types.pi_map_π_apply'
 
 /-- The category of types has `PUnit` as a terminal object. -/
@@ -339,7 +337,8 @@ noncomputable def isCoprodOfMono {X Y : Type u} (f : X ⟶ Y) [Mono f] :
   exact Subtype.range_val
 #align category_theory.limits.types.is_coprod_of_mono CategoryTheory.Limits.Types.isCoprodOfMono
 
-/-- The category of types has `Π j, f j` as the product of a type family `f : J → Type`.
+/--
+The category of types has `Π j, f j` as the product of a type family `f : J → TypeMax.{v, u}`.
 -/
 def productLimitCone {J : Type v} (F : J → TypeMax.{v, u}) :
     Limits.LimitCone (Discrete.functor F) where
@@ -351,7 +350,7 @@ def productLimitCone {J : Type v} (F : J → TypeMax.{v, u}) :
       uniq := fun s m w => funext fun x => funext fun j => (congr_fun (w ⟨j⟩) x : _) }
 #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`. -/
+/-- The categorical product in `TypeMax.{v, u}` is the type theoretic product `Π j, F j`. -/
 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
@@ -376,6 +375,46 @@ theorem productIso_inv_comp_π {J : Type v} (F : J → TypeMax.{v, u}) (j : J) :
   limit.isoLimitCone_inv_π (productLimitCone.{v, u} F) ⟨j⟩
 #align category_theory.limits.types.product_iso_inv_comp_π CategoryTheory.Limits.Types.productIso_inv_comp_π
 
+namespace UnivLE
+
+/--
+A variant of `productLimitCone` using a `UnivLE` hypothesis rather than a function to `TypeMax`.
+-/
+noncomputable def productLimitCone {J : Type v} (F : J → Type u) [UnivLE.{v, u}] :
+    Limits.LimitCone (Discrete.functor F) where
+  cone :=
+    { pt := Shrink (∀ j, F j)
+      π := Discrete.natTrans (fun ⟨j⟩ f => (equivShrink _).symm f j) }
+  isLimit :=
+    { lift := fun s x => (equivShrink _) (fun j => s.π.app ⟨j⟩ x)
+      uniq := fun s m w => funext fun x => Shrink.ext <| funext fun j => by
+        simpa using (congr_fun (w ⟨j⟩) x : _) }
+
+/-- The categorical product in `Type u` indexed in `Type v`
+is the type theoretic product `Π j, F j`, after shrinking back to `Type u`. -/
+noncomputable def productIso {J : Type v} (F : J → Type u) [UnivLE.{v, u}] :
+    (∏ F : Type u) ≅ Shrink.{u} (∀ j, F j) :=
+  limit.isoLimitCone (productLimitCone.{v, u} F)
+
+@[simp]
+theorem productIso_hom_comp_eval {J : Type v} (F : J → Type u) [UnivLE.{v, u}] (j : J) :
+    ((productIso.{v, u} F).hom ≫ fun f => (equivShrink _).symm f j) = Pi.π F j :=
+  limit.isoLimitCone_hom_π (productLimitCone.{v, u} F) ⟨j⟩
+
+-- Porting note:
+-- `elementwise` seems to be broken. Applied to the previous lemma, it should produce:
+@[simp]
+theorem productIso_hom_comp_eval_apply {J : Type v} (F : J → Type u) [UnivLE.{v, u}] (j : J) (x) :
+   (equivShrink _).symm ((productIso F).hom x) j = Pi.π F j x :=
+  congr_fun (productIso_hom_comp_eval F j) x
+
+@[elementwise (attr := simp)]
+theorem productIso_inv_comp_π {J : Type v} (F : J → Type u) [UnivLE.{v, u}] (j : J) :
+    (productIso.{v, u} F).inv ≫ Pi.π F j = fun f => ((equivShrink _).symm f) j :=
+  limit.isoLimitCone_inv_π (productLimitCone.{v, u} F) ⟨j⟩
+
+end UnivLE
+
 /-- The category of types has `Σ j, f j` as the coproduct of a type family `f : J → Type`.
 -/
 def coproductColimitCocone {J : Type u} (F : J → Type u) :
@@ -556,6 +595,13 @@ end Cofork
 
 section Pullback
 
+-- #synth HasPullbacks.{u} (Type u)
+instance : HasPullbacks.{u} (Type u) :=
+  -- FIXME does not work via `inferInstance` despite `#synth HasPullbacks.{u} (Type u)` succeeding.
+  -- https://github.com/leanprover-community/mathlib4/issues/5752
+  -- inferInstance
+  hasPullbacks_of_hasWidePullbacks.{u} (Type u)
+
 open CategoryTheory.Limits.WalkingPair
 
 open CategoryTheory.Limits.WalkingCospan
@@ -639,4 +685,15 @@ theorem pullbackIsoPullback_inv_snd :
 
 end Pullback
 
+section Pushout
+
+-- #synth HasPushouts.{u} (Type u)
+instance : HasPushouts.{u} (Type u) :=
+  -- FIXME does not work via `inferInstance` despite `#synth HasPushouts.{u} (Type u)` succeeding.
+  -- https://github.com/leanprover-community/mathlib4/issues/5752
+  -- inferInstance
+  hasPushouts_of_hasWidePushouts.{u} (Type u)
+
+end Pushout
+
 end CategoryTheory.Limits.Types