feat: use pp_with_univ (#5622)

Certain definitions do nothing except change universes. We might as well have the pretty printer always show us these universes!



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

Mathlib/CategoryTheory/Limits/Creates.lean

@@ -93,6 +93,8 @@ class CreatesLimitsOfSize (F : C ⥤ D) where
     infer_instance
 #align category_theory.creates_limits_of_size CategoryTheory.CreatesLimitsOfSize
 
+pp_with_univ CreatesLimitsOfSize
+
 /-- `F` creates small limits if it creates limits of shape `J` for any small `J`. -/
 abbrev CreatesLimits (F : C ⥤ D) :=
   CreatesLimitsOfSize.{v₂, v₂} F
@@ -126,6 +128,8 @@ class CreatesColimitsOfSize (F : C ⥤ D) where
     infer_instance
 #align category_theory.creates_colimits_of_size CategoryTheory.CreatesColimitsOfSize
 
+pp_with_univ CreatesColimitsOfSize
+
 /-- `F` creates small colimits if it creates colimits of shape `J` for any small `J`. -/
 abbrev CreatesColimits (F : C ⥤ D) :=
   CreatesColimitsOfSize.{v₂, v₂} F

Mathlib/CategoryTheory/Limits/Filtered.lean

@@ -36,12 +36,16 @@ class HasCofilteredLimitsOfSize : Prop where
   HasLimitsOfShape : ∀ (I : Type w) [Category.{w'} I] [IsCofiltered I], HasLimitsOfShape I C
 #align category_theory.limits.has_cofiltered_limits_of_size CategoryTheory.Limits.HasCofilteredLimitsOfSize
 
+pp_with_univ HasCofilteredLimitsOfSize
+
 /-- Class for having all filtered colimits of a given size. -/
 class HasFilteredColimitsOfSize : Prop where
   /-- For all filtered types of a size `w`, we have colimits -/
   HasColimitsOfShape : ∀ (I : Type w) [Category.{w'} I] [IsFiltered I], HasColimitsOfShape I C
 #align category_theory.limits.has_filtered_colimits_of_size CategoryTheory.Limits.HasFilteredColimitsOfSize
 
+pp_with_univ HasFilteredColimitsOfSize
+
 end
 
 instance (priority := 100) hasLimitsOfShape_of_has_cofiltered_limits
@@ -57,4 +61,3 @@ instance (priority := 100) hasColimitsOfShape_of_has_filtered_colimits
 #align category_theory.limits.has_colimits_of_shape_of_has_filtered_colimits CategoryTheory.Limits.hasColimitsOfShape_of_has_filtered_colimits
 
 end CategoryTheory.Limits
-

Mathlib/CategoryTheory/Limits/HasLimits.lean

@@ -117,6 +117,8 @@ class HasLimitsOfSize (C : Type u) [Category.{v} C] : Prop where
     infer_instance
 #align category_theory.limits.has_limits_of_size CategoryTheory.Limits.HasLimitsOfSize
 
+pp_with_univ HasLimitsOfSize
+
 /-- `C` has all (small) limits if it has limits of every shape that is as big as its hom-sets. -/
 abbrev HasLimits (C : Type u) [Category.{v} C] : Prop :=
   HasLimitsOfSize.{v, v} C
@@ -671,6 +673,8 @@ class HasColimitsOfSize (C : Type u) [Category.{v} C] : Prop where
     infer_instance
 #align category_theory.limits.has_colimits_of_size CategoryTheory.Limits.HasColimitsOfSize
 
+pp_with_univ HasColimitsOfSize
+
 /-- `C` has all (small) colimits if it has colimits of every shape that is as big as its hom-sets.
 -/
 abbrev HasColimits (C : Type u) [Category.{v} C] : Prop :=

Mathlib/CategoryTheory/Limits/Preserves/Basic.lean

@@ -91,6 +91,8 @@ class PreservesLimitsOfSize (F : C ⥤ D) where
 #align category_theory.limits.preserves_limits_of_size CategoryTheory.Limits.PreservesLimitsOfSize
 #align category_theory.limits.preserves_limits_of_size.preserves_limits_of_shape CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape
 
+pp_with_univ PreservesLimitsOfSize
+
 /-- We say that `F` preserves (small) limits if it sends small
 limit cones over any diagram to limit cones. -/
 abbrev PreservesLimits (F : C ⥤ D) :=
@@ -107,6 +109,8 @@ class PreservesColimitsOfSize (F : C ⥤ D) where
 #align category_theory.limits.preserves_colimits_of_size CategoryTheory.Limits.PreservesColimitsOfSize
 #align category_theory.limits.preserves_colimits_of_size.preserves_colimits_of_shape CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape
 
+pp_with_univ PreservesColimitsOfSize
+
 /-- We say that `F` preserves (small) limits if it sends small
 limit cones over any diagram to limit cones. -/
 abbrev PreservesColimits (F : C ⥤ D) :=
@@ -403,6 +407,8 @@ class ReflectsLimitsOfSize (F : C ⥤ D) where
     infer_instance
 #align category_theory.limits.reflects_limits_of_size CategoryTheory.Limits.ReflectsLimitsOfSize
 
+pp_with_univ ReflectsLimitsOfSize
+
 /-- A functor `F : C ⥤ D` reflects (small) limits if
 whenever the image of a cone over some `K : J ⥤ C` under `F` is a limit cone in `D`,
 the cone was already a limit cone in `C`.
@@ -424,6 +430,8 @@ class ReflectsColimitsOfSize (F : C ⥤ D) where
     infer_instance
 #align category_theory.limits.reflects_colimits_of_size CategoryTheory.Limits.ReflectsColimitsOfSize
 
+pp_with_univ ReflectsColimitsOfSize
+
 /-- A functor `F : C ⥤ D` reflects (small) colimits if
 whenever the image of a cocone over some `K : J ⥤ C` under `F` is a colimit cocone in `D`,
 the cocone was already a colimit cocone in `C`.

Mathlib/CategoryTheory/Types.lean

@@ -12,6 +12,7 @@ import Mathlib.CategoryTheory.EpiMono
 import Mathlib.CategoryTheory.Functor.FullyFaithful
 import Mathlib.Logic.Equiv.Basic
 import Mathlib.Data.Set.Basic
+import Mathlib.Tactic.PPWithUniv
 
 /-!
 # The category `Type`.
@@ -197,14 +198,16 @@ def uliftTrivial (V : Type u) : ULift.{u} V ≅ V where
 #align category_theory.ulift_trivial CategoryTheory.uliftTrivial
 
 /-- The functor embedding `Type u` into `Type (max u v)`.
-Write this as `uliftFunctor.{5 2}` to get `Type 2 ⥤ Type 5`.
+Write this as `uliftFunctor.{5, 2}` to get `Type 2 ⥤ Type 5`.
 -/
 def uliftFunctor : Type u ⥤ Type max u v
     where
   obj X := ULift.{v} X
   map {X} {Y} f := fun x : ULift.{v} X => ULift.up (f x.down)
 #align category_theory.ulift_functor CategoryTheory.uliftFunctor
 
+pp_with_univ uliftFunctor
+
 @[simp]
 theorem uliftFunctor_map {X Y : Type u} (f : X ⟶ Y) (x : ULift.{v} X) :
     uliftFunctor.map f x = ULift.up (f x.down) :=

Mathlib/Logic/Small/Basic.lean

@@ -9,6 +9,7 @@ Authors: Scott Morrison
 ! if you have ported upstream changes.
 -/
 import Mathlib.Logic.Equiv.Set
+import Mathlib.Tactic.PPWithUniv
 
 /-!
 # Small types
@@ -32,6 +33,8 @@ class Small (α : Type v) : Prop where
   equiv_small : ∃ S : Type w, Nonempty (α ≃ S)
 #align small Small
 
+pp_with_univ Small
+
 /-- Constructor for `Small α` from an explicit witness type and equivalence.
 -/
 theorem Small.mk' {α : Type v} {S : Type w} (e : α ≃ S) : Small.{w} α :=