chore(category_theory): remove [𝒞 : category.{v₁} C] / include 𝒞 (#…

…2556)

It is no longer necessary in Lean 3.9.0, thanks to
leanprover-community/lean@0106385

docs/theories/category_theory.md

@@ -42,20 +42,6 @@ a small category. If `C` is a small category and `D` is a large category
 (i.e. `u₂ = v₂+1`), and `v₂ = v₁` then we have
 `functor.category C D : category.{v₁+1}` so is again a large category.
 
-Whenever you want to write code uniformly for small and large categories
-(which you do by talking about categories whose universe levels `u` and `v`
-are unrelated), you will find that Lean's `variable` mechanism doesn't always
-work, and the following trick is often helpful:
-
-````
-variables {C : Type u₁} [𝒞 : category.{v₁} C]
-variables {D : Type u₂} [𝒟 : category.{v₂} D]
-include 𝒞 𝒟
-````
-
-Some care with using `section ... end` can be required to make sure these
-included variables don't end up where they aren't wanted.
-
 ## Notation
 
 ### Categories

src/category_theory/adjunction/basic.lean

@@ -13,8 +13,7 @@ universes v₁ v₂ v₃ u₁ u₂ u₃ -- declare the `v`'s first; see `categor
 
 local attribute [elab_simple] whisker_left whisker_right
 
-variables {C : Type u₁} [𝒞 : category.{v₁} C] {D : Type u₂} [𝒟 : category.{v₂} D]
-include 𝒞 𝒟
+variables {C : Type u₁} [category.{v₁} C] {D : Type u₂} [category.{v₂} D]
 
 /--
 `F ⊣ G` represents the data of an adjunction between two functors
@@ -200,16 +199,11 @@ def mk_of_unit_counit (adj : core_unit_counit F G) : F ⊣ G :=
   end },
   .. adj }
 
-section
-omit 𝒟
-
 def id : 𝟭 C ⊣ 𝟭 C :=
 { hom_equiv := λ X Y, equiv.refl _,
   unit := 𝟙 _,
   counit := 𝟙 _ }
 
-end
-
 section
 variables {E : Type u₃} [ℰ : category.{v₃} E] (H : D ⥤ E) (I : E ⥤ D)
 

src/category_theory/adjunction/fully_faithful.lean

@@ -14,9 +14,8 @@ universes v₁ v₂ u₁ u₂
 open category
 open opposite
 
-variables {C : Type u₁} [𝒞 : category.{v₁} C]
-variables {D : Type u₂} [𝒟 : category.{v₂} D]
-include 𝒞 𝒟
+variables {C : Type u₁} [category.{v₁} C]
+variables {D : Type u₂} [category.{v₂} D]
 variables {L : C ⥤ D} {R : D ⥤ C} (h : L ⊣ R)
 
 -- Lemma 4.5.13 from [Riehl][riehl2017]

src/category_theory/adjunction/limits.lean

@@ -15,8 +15,7 @@ open category_theory.limits
 
 universes u₁ u₂ v
 
-variables {C : Type u₁} [𝒞 : category.{v} C] {D : Type u₂} [𝒟 : category.{v} D]
-include 𝒞 𝒟
+variables {C : Type u₁} [category.{v} C] {D : Type u₂} [category.{v} D]
 
 variables {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G)
 include adj

src/category_theory/category/default.lean

@@ -86,8 +86,7 @@ A `small_category` has objects and morphisms in the same universe level.
 abbreviation small_category (C : Type u) : Type (u+1) := category.{u} C
 
 section
-variables {C : Type u} [𝒞 : category.{v} C] {X Y Z : C}
-include 𝒞
+variables {C : Type u} [category.{v} C] {X Y Z : C}
 
 /-- postcompose an equation between morphisms by another morphism -/
 lemma eq_whisker {f g : X ⟶ Y} (w : f = g) (h : Y ⟶ Z) : f ≫ h = g ≫ h :=

src/category_theory/comma.lean

@@ -51,10 +51,9 @@ comma, slice, coslice, over, under, arrow
 namespace category_theory
 
 universes v₁ v₂ v₃ u₁ u₂ u₃ -- declare the `v`'s first; see `category_theory.category` for an explanation
-variables {A : Type u₁} [𝒜 : category.{v₁} A]
-variables {B : Type u₂} [ℬ : category.{v₂} B]
-variables {T : Type u₃} [𝒯 : category.{v₃} T]
-include 𝒜 ℬ 𝒯
+variables {A : Type u₁} [category.{v₁} A]
+variables {B : Type u₂} [category.{v₂} B]
+variables {T : Type u₃} [category.{v₃} T]
 
 /-- The objects of the comma category are triples of an object `left : A`, an object
    `right : B` and a morphism `hom : L.obj left ⟶ R.obj right`.  -/
@@ -63,18 +62,13 @@ structure comma (L : A ⥤ T) (R : B ⥤ T) : Type (max u₁ u₂ v₃) :=
 (right : B . obviously)
 (hom : L.obj left ⟶ R.obj right)
 
-section
-omit 𝒜 ℬ
-
 -- Satisfying the inhabited linter
 instance comma.inhabited [inhabited T] : inhabited (comma (𝟭 T) (𝟭 T)) :=
 { default :=
   { left := default T,
     right := default T,
     hom := 𝟙 (default T) } }
 
-end
-
 variables {L : A ⥤ T} {R : B ⥤ T}
 
 /-- A morphism between two objects in the comma category is a commutative square connecting the
@@ -265,8 +259,6 @@ end
 
 end comma
 
-omit 𝒜 ℬ
-
 /-- The over category has as objects arrows in `T` with codomain `X` and as morphisms commutative
     triangles. -/
 @[derive category]
@@ -378,8 +370,7 @@ rfl
 end iterated_slice
 
 section
-variables {D : Type u₃} [𝒟 : category.{v₃} D]
-include 𝒟
+variables {D : Type u₃} [category.{v₃} D]
 
 /-- A functor `F : T ⥤ D` induces a functor `over X ⥤ over (F.obj X)` in the obvious way. -/
 def post (F : T ⥤ D) : over X ⥤ over (F.obj X) :=
@@ -455,8 +446,7 @@ variables {Y : T} {f : X ⟶ Y} {U V : under Y} {g : U ⟶ V}
 end
 
 section
-variables {D : Type u₃} [𝒟 : category.{v₃} D]
-include 𝒟
+variables {D : Type u₃} [category.{v₃} D]
 
 /-- A functor `F : T ⥤ D` induces a functor `under X ⥤ under (F.obj X)` in the obvious way. -/
 def post {X : T} (F : T ⥤ D) : under X ⥤ under (F.obj X) :=

src/category_theory/connected.lean

@@ -58,12 +58,11 @@ component'.
 
 This allows us to show that the functor X ⨯ - preserves connected limits.
 -/
-class connected (J : Type v₂) [𝒥 : category.{v₁} J] extends inhabited J :=
+class connected (J : Type v₂) [category.{v₁} J] extends inhabited J :=
 (iso_constant : Π {α : Type v₂} (F : J ⥤ discrete α), F ≅ (functor.const J).obj (F.obj default))
 end connected
 
-variables {J : Type v₂} [𝒥 : category.{v₁} J]
-include 𝒥
+variables {J : Type v₂} [category.{v₁} J]
 
 /--
 If J is connected, any functor to a discrete category is constant on objects.
@@ -203,8 +202,7 @@ begin
   { exact (k a).1 }
 end
 
-variables {C : Type u₂} [𝒞 : category.{v₂} C]
-include 𝒞
+variables {C : Type u₂} [category.{v₂} C]
 
 /--
 For objects `X Y : C`, any natural transformation `α : const X ⟶ const Y` from a connected

src/category_theory/const.lean

@@ -11,9 +11,8 @@ open category_theory
 
 namespace category_theory.functor
 
-variables (J : Type u₁) [𝒥 : category.{v₁} J]
-variables {C : Type u₂} [𝒞 : category.{v₂} C]
-include 𝒥 𝒞
+variables (J : Type u₁) [category.{v₁} J]
+variables {C : Type u₂} [category.{v₂} C]
 
 def const : C ⥤ (J ⥤ C) :=
 { obj := λ X,
@@ -54,8 +53,7 @@ end const
 
 
 section
-variables {D : Type u₃} [𝒟 : category.{v₃} D]
-include 𝒟
+variables {D : Type u₃} [category.{v₃} D]
 
 /-- These are actually equal, of course, but not definitionally equal
   (the equality requires F.map (𝟙 _) = 𝟙 _). A natural isomorphism is

src/category_theory/core.lean

@@ -15,8 +15,7 @@ universes v₁ v₂ u₁ u₂ -- declare the `v`'s first; see `category_theory.c
 isomorphisms of C. -/
 def core (C : Type u₁) := C
 
-variables {C : Type u₁} [𝒞 : category.{v₁} C]
-include 𝒞
+variables {C : Type u₁} [category.{v₁} C]
 
 instance core_category : groupoid.{v₁} (core C) :=
 { hom  := λ X Y : C, X ≅ Y,
@@ -34,8 +33,7 @@ def inclusion : core C ⥤ C :=
 { obj := id,
   map := λ X Y f, f.hom }
 
-variables {G : Type u₂} [𝒢 : groupoid.{v₂} G]
-include 𝒢
+variables {G : Type u₂} [groupoid.{v₂} G]
 
 /-- A functor from a groupoid to a category C factors through the core of C. -/
 -- Note that this function is not functorial
@@ -47,8 +45,6 @@ def functor_to_core (F : G ⥤ C) : G ⥤ core C :=
 def forget_functor_to_core : (G ⥤ core C) ⥤ (G ⥤ C) := (whiskering_right _ _ _).obj inclusion
 end core
 
-omit 𝒞
-
 /--
 `of_equiv_functor m` lifts a type-level `equiv_functor`
 to a categorical functor `core (Type u₁) ⥤ core (Type u₂)`.

src/category_theory/currying.lean

@@ -9,10 +9,9 @@ namespace category_theory
 
 universes v₁ v₂ v₃ u₁ u₂ u₃
 
-variables {C : Type u₁} [𝒞 : category.{v₁} C]
-          {D : Type u₂} [𝒟 : category.{v₂} D]
-          {E : Type u₃} [ℰ : category.{v₃} E]
-include 𝒞 𝒟 ℰ
+variables {C : Type u₁} [category.{v₁} C]
+          {D : Type u₂} [category.{v₂} D]
+          {E : Type u₃} [category.{v₃} E]
 
 def uncurry : (C ⥤ (D ⥤ E)) ⥤ ((C × D) ⥤ E) :=
 { obj := λ F,

src/category_theory/differential_object.lean

@@ -23,8 +23,7 @@ universes v u
 
 namespace category_theory
 
-variables (C : Type u) [𝒞 : category.{v} C]
-include 𝒞
+variables (C : Type u) [category.{v} C]
 
 variables [has_zero_morphisms.{v} C] [has_shift.{v} C]
 
@@ -111,8 +110,7 @@ namespace category_theory
 
 namespace differential_object
 
-variables (C : Type u) [𝒞 : category.{v} C]
-include 𝒞
+variables (C : Type u) [category.{v} C]
 
 variables [has_zero_object.{v} C] [has_zero_morphisms.{v} C] [has_shift.{v} C]
 
@@ -129,9 +127,8 @@ end differential_object
 
 namespace differential_object
 
-variables (C : Type (u+1)) [large_category C] [𝒞 : concrete_category C]
+variables (C : Type (u+1)) [large_category C] [concrete_category C]
   [has_zero_morphisms.{u} C] [has_shift.{u} C]
-include 𝒞
 
 instance concrete_category_of_differential_objects :
   concrete_category (differential_object.{u} C) :=

src/category_theory/discrete_category.lean

@@ -35,8 +35,7 @@ by { apply ulift.fintype }
 
 end discrete
 
-variables {C : Type u₂} [𝒞 : category.{v₂} C]
-include 𝒞
+variables {C : Type u₂} [category.{v₂} C]
 
 namespace functor
 
@@ -80,8 +79,6 @@ end nat_iso
 namespace discrete
 variables {J : Type v₁}
 
-omit 𝒞
-
 def lift {α : Type u₁} {β : Type u₂} (f : α → β) : (discrete α) ⥤ (discrete β) :=
 functor.of_function f
 
@@ -94,7 +91,6 @@ begin
   refine nat_iso.of_components (λ X, by simp [F]) _,
   tidy
 end
-include 𝒞
 
 
 @[simp] lemma functor_map_id

src/category_theory/endomorphism.lean

@@ -49,8 +49,7 @@ instance group {C : Type u} [groupoid.{v} C] (X : C) : group (End X) :=
 
 end End
 
-variables {C : Type u} [𝒞 : category.{v} C] (X : C)
-include 𝒞
+variables {C : Type u} [category.{v} C] (X : C)
 
 def Aut (X : C) := X ≅ X
 
@@ -78,8 +77,7 @@ end Aut
 
 namespace functor
 
-variables {D : Type u'} [𝒟 : category.{v'} D] (f : C ⥤ D) (X)
-include 𝒟
+variables {D : Type u'} [category.{v'} D] (f : C ⥤ D) (X)
 
 /-- `f.map` as a monoid hom between endomorphism monoids. -/
 def map_End : End X →* End (f.obj X) :=

src/category_theory/epi_mono.lean

@@ -15,12 +15,10 @@ universes v₁ v₂ u₁ u₂
 
 namespace category_theory
 
-variables {C : Type u₁} [𝒞 : category.{v₁} C]
-include 𝒞
+variables {C : Type u₁} [category.{v₁} C]
 
 section
-variables {D : Type u₂} [𝒟 : category.{v₂} D]
-include 𝒟
+variables {D : Type u₂} [category.{v₂} D]
 
 lemma left_adjoint_preserves_epi {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G)
   {X Y : C} {f : X ⟶ Y} (hf : epi f) : epi (F.map f) :=
@@ -140,8 +138,7 @@ instance op_epi_of_mono {A B : C} (f : A ⟶ B) [mono f] : epi f.op :=
 ⟨λ Z g h eq, has_hom.hom.unop_inj ((cancel_mono f).1 (has_hom.hom.op_inj eq))⟩
 
 section
-variables {D : Type u₂} [𝒟 : category.{v₂} D]
-include 𝒟
+variables {D : Type u₂} [category.{v₂} D]
 
 /-- Split monomorphisms are also absolute monomorphisms. -/
 instance {X Y : C} (f : X ⟶ Y) [split_mono f] (F : C ⥤ D) : split_mono (F.map f) :=

src/category_theory/eq_to_hom.lean

@@ -10,8 +10,7 @@ universes v v' u u' -- declare the `v`'s first; see `category_theory.category` f
 namespace category_theory
 open opposite
 
-variables {C : Type u} [𝒞 : category.{v} C]
-include 𝒞
+variables {C : Type u} [category.{v} C]
 
 def eq_to_hom {X Y : C} (p : X = Y) : X ⟶ Y := by rw p; exact 𝟙 _
 
@@ -39,8 +38,7 @@ begin
   refl
 end
 
-variables {D : Type u'} [𝒟 : category.{v'} D]
-include 𝒟
+variables {D : Type u'} [category.{v'} D]
 
 namespace functor