chore(category_theory/limits): Generalize universe for preserving lim…

…its (#10736)

src/category_theory/closed/functor.lean

@@ -64,7 +64,7 @@ If `F` is full and faithful and has a left adjoint `L` which preserves binary pr
 Frobenius morphism is an isomorphism.
 -/
 instance frobenius_morphism_iso_of_preserves_binary_products (h : L ⊣ F) (A : C)
-  [preserves_limits_of_shape (discrete walking_pair) L] [full F] [faithful F] :
+  [preserves_limits_of_shape (discrete.{v} walking_pair) L] [full F] [faithful F] :
 is_iso (frobenius_morphism F h A) :=
 begin
   apply nat_iso.is_iso_of_is_iso_app _,
@@ -74,7 +74,7 @@ begin
 end
 
 variables [cartesian_closed C] [cartesian_closed D]
-variables [preserves_limits_of_shape (discrete walking_pair) F]
+variables [preserves_limits_of_shape (discrete.{v} walking_pair) F]
 
 /--
 The exponential comparison map.
@@ -182,7 +182,7 @@ TODO: Show the converse, that if `F` is cartesian closed and its left adjoint pr
 products, then it is full and faithful.
 -/
 def cartesian_closed_functor_of_left_adjoint_preserves_binary_products (h : L ⊣ F)
-  [full F] [faithful F] [preserves_limits_of_shape (discrete walking_pair) L] :
+  [full F] [faithful F] [preserves_limits_of_shape (discrete.{v} walking_pair) L] :
   cartesian_closed_functor F :=
 { comparison_iso := λ A, exp_comparison_iso_of_frobenius_morphism_iso F h _ }
 

src/category_theory/closed/ideal.lean

@@ -124,7 +124,7 @@ This is the converse of `preserves_binary_products_of_exponential_ideal`.
 -/
 @[priority 10]
 instance exponential_ideal_of_preserves_binary_products
-  [preserves_limits_of_shape (discrete walking_pair) (left_adjoint i)] :
+  [preserves_limits_of_shape (discrete.{v₁} walking_pair) (left_adjoint i)] :
   exponential_ideal i :=
 begin
   let ir := adjunction.of_right_adjoint i,

src/category_theory/limits/comma.lean

@@ -203,7 +203,7 @@ noncomputable instance creates_limits_of_shape [preserves_limits_of_shape J G] :
   creates_limits_of_shape J (proj X G) := {}
 
 noncomputable instance creates_limits [preserves_limits G] :
-  creates_limits (proj X G : _) := {}
+  creates_limits (proj X G : _) := ⟨⟩
 
 end structured_arrow
 
@@ -232,7 +232,7 @@ noncomputable instance creates_colimits_of_shape [preserves_colimits_of_shape J
   creates_colimits_of_shape J (proj G X) := {}
 
 noncomputable instance creates_colimits [preserves_colimits G] :
-  creates_colimits (proj G X : _) := {}
+  creates_colimits (proj G X : _) := ⟨⟩
 
 end costructured_arrow
 

src/category_theory/limits/constructions/finite_products_of_binary_products.lean

@@ -144,20 +144,20 @@ end
 
 section preserves
 variables (F : C ⥤ D)
-variables [preserves_limits_of_shape (discrete walking_pair) F]
-variables [preserves_limits_of_shape (discrete pempty) F]
+variables [preserves_limits_of_shape (discrete.{v} walking_pair) F]
+variables [preserves_limits_of_shape (discrete.{v} pempty) F]
 variables [has_finite_products.{v} C]
 
 /--
 If `F` preserves the terminal object and binary products, then it preserves products indexed by
 `ulift (fin n)` for any `n`.
 -/
 noncomputable def preserves_fin_of_preserves_binary_and_terminal  :
-  Π (n : ℕ) (f : ulift (fin n) → C), preserves_limit (discrete.functor f) F
+  Π (n : ℕ) (f : ulift.{v} (fin n) → C), preserves_limit (discrete.functor f) F
 | 0 := λ f,
   begin
     letI : preserves_limits_of_shape (discrete (ulift (fin 0))) F :=
-      preserves_limits_of_shape_of_equiv
+      preserves_limits_of_shape_of_equiv.{v v}
         (discrete.equivalence (equiv.ulift.trans fin_zero_equiv').symm) _,
     apply_instance,
   end
@@ -206,7 +206,8 @@ begin
   classical,
   let e := fintype.equiv_fin J,
   haveI := preserves_ulift_fin_of_preserves_binary_and_terminal F (fintype.card J),
-  apply preserves_limits_of_shape_of_equiv (discrete.equivalence (e.trans equiv.ulift.symm)).symm,
+  apply preserves_limits_of_shape_of_equiv.{v v}
+    (discrete.equivalence (e.trans equiv.ulift.symm)).symm,
 end
 
 end preserves
@@ -323,20 +324,20 @@ end
 
 section preserves
 variables (F : C ⥤ D)
-variables [preserves_colimits_of_shape (discrete walking_pair) F]
-variables [preserves_colimits_of_shape (discrete pempty) F]
+variables [preserves_colimits_of_shape (discrete.{v} walking_pair) F]
+variables [preserves_colimits_of_shape (discrete.{v} pempty) F]
 variables [has_finite_coproducts.{v} C]
 
 /--
 If `F` preserves the initial object and binary coproducts, then it preserves products indexed by
 `ulift (fin n)` for any `n`.
 -/
 noncomputable def preserves_fin_of_preserves_binary_and_initial  :
-  Π (n : ℕ) (f : ulift (fin n) → C), preserves_colimit (discrete.functor f) F
+  Π (n : ℕ) (f : ulift.{v} (fin n) → C), preserves_colimit (discrete.functor f) F
 | 0 := λ f,
   begin
     letI : preserves_colimits_of_shape (discrete (ulift (fin 0))) F :=
-      preserves_colimits_of_shape_of_equiv
+      preserves_colimits_of_shape_of_equiv.{v v}
         (discrete.equivalence (equiv.ulift.trans fin_zero_equiv').symm) _,
     apply_instance,
   end
@@ -384,7 +385,8 @@ begin
   classical,
   let e := fintype.equiv_fin J,
   haveI := preserves_ulift_fin_of_preserves_binary_and_initial F (fintype.card J),
-  apply preserves_colimits_of_shape_of_equiv (discrete.equivalence (e.trans equiv.ulift.symm)).symm,
+  apply preserves_colimits_of_shape_of_equiv.{v v}
+    (discrete.equivalence (e.trans equiv.ulift.symm)).symm,
 end
 
 end preserves

src/category_theory/limits/constructions/limits_of_products_and_equalizers.lean

@@ -126,13 +126,13 @@ noncomputable theory
 
 section
 
-variables [has_limits_of_shape (discrete J) C]
-          [has_limits_of_shape (discrete (Σ p : J × J, p.1 ⟶ p.2)) C]
+variables [has_limits_of_shape (discrete.{v} J) C]
+          [has_limits_of_shape (discrete.{v} (Σ p : J × J, p.1 ⟶ p.2)) C]
           [has_equalizers C]
 variables (G : C ⥤ D)
-          [preserves_limits_of_shape walking_parallel_pair G]
-          [preserves_limits_of_shape (discrete J) G]
-          [preserves_limits_of_shape (discrete (Σ p : J × J, p.1 ⟶ p.2)) G]
+          [preserves_limits_of_shape walking_parallel_pair.{v} G]
+          [preserves_limits_of_shape (discrete.{v} J) G]
+          [preserves_limits_of_shape (discrete.{v} (Σ p : J × J, p.1 ⟶ p.2)) G]
 
 /-- If a functor preserves equalizers and the appropriate products, it preserves limits. -/
 def preserves_limit_of_preserves_equalizers_and_product :
@@ -177,16 +177,16 @@ end
 /-- If G preserves equalizers and finite products, it preserves finite limits. -/
 def preserves_finite_limits_of_preserves_equalizers_and_finite_products
   [has_equalizers C] [has_finite_products C]
-  (G : C ⥤ D) [preserves_limits_of_shape walking_parallel_pair G]
-  [∀ J [fintype J], preserves_limits_of_shape (discrete J) G] :
+  (G : C ⥤ D) [preserves_limits_of_shape walking_parallel_pair.{v} G]
+  [∀ J [fintype J], preserves_limits_of_shape (discrete.{v} J) G] :
   preserves_finite_limits G :=
 ⟨λ _ _ _, by exactI preserves_limit_of_preserves_equalizers_and_product G⟩
 
 /-- If G preserves equalizers and products, it preserves all limits. -/
 def preserves_limits_of_preserves_equalizers_and_products
   [has_equalizers C] [has_products C]
-  (G : C ⥤ D) [preserves_limits_of_shape walking_parallel_pair G]
-  [∀ J, preserves_limits_of_shape (discrete J) G] :
+  (G : C ⥤ D) [preserves_limits_of_shape walking_parallel_pair.{v} G]
+  [∀ J, preserves_limits_of_shape (discrete.{v} J) G] :
 preserves_limits G :=
 { preserves_limits_of_shape := λ J 𝒥,
   by exactI preserves_limit_of_preserves_equalizers_and_product G }
@@ -286,13 +286,13 @@ noncomputable theory
 
 section
 
-variables [has_colimits_of_shape (discrete J) C]
-          [has_colimits_of_shape (discrete (Σ p : J × J, p.1 ⟶ p.2)) C]
+variables [has_colimits_of_shape (discrete.{v} J) C]
+          [has_colimits_of_shape (discrete.{v} (Σ p : J × J, p.1 ⟶ p.2)) C]
           [has_coequalizers C]
 variables (G : C ⥤ D)
-          [preserves_colimits_of_shape walking_parallel_pair G]
-          [preserves_colimits_of_shape (discrete J) G]
-          [preserves_colimits_of_shape (discrete (Σ p : J × J, p.1 ⟶ p.2)) G]
+          [preserves_colimits_of_shape walking_parallel_pair.{v} G]
+          [preserves_colimits_of_shape (discrete.{v} J) G]
+          [preserves_colimits_of_shape (discrete.{v} (Σ p : J × J, p.1 ⟶ p.2)) G]
 
 /-- If a functor preserves coequalizers and the appropriate coproducts, it preserves colimits. -/
 def preserves_colimit_of_preserves_coequalizers_and_coproduct :
@@ -337,16 +337,16 @@ end
 /-- If G preserves coequalizers and finite coproducts, it preserves finite colimits. -/
 def preserves_finite_colimits_of_preserves_coequalizers_and_finite_coproducts
   [has_coequalizers C] [has_finite_coproducts C]
-  (G : C ⥤ D) [preserves_colimits_of_shape walking_parallel_pair G]
-  [∀ J [fintype J], preserves_colimits_of_shape (discrete J) G] :
+  (G : C ⥤ D) [preserves_colimits_of_shape walking_parallel_pair.{v} G]
+  [∀ J [fintype J], preserves_colimits_of_shape (discrete.{v} J) G] :
   preserves_finite_colimits G :=
 ⟨λ _ _ _, by exactI preserves_colimit_of_preserves_coequalizers_and_coproduct G⟩
 
 /-- If G preserves coequalizers and coproducts, it preserves all colimits. -/
 def preserves_colimits_of_preserves_coequalizers_and_coproducts
   [has_coequalizers C] [has_coproducts C]
-  (G : C ⥤ D) [preserves_colimits_of_shape walking_parallel_pair G]
-  [∀ J, preserves_colimits_of_shape (discrete J) G] :
+  (G : C ⥤ D) [preserves_colimits_of_shape walking_parallel_pair.{v} G]
+  [∀ J, preserves_colimits_of_shape (discrete.{v} J) G] :
 preserves_colimits G :=
 { preserves_colimits_of_shape := λ J 𝒥,
   by exactI preserves_colimit_of_preserves_coequalizers_and_coproduct G }