leanprover-community · mo271 · Feb 18, 2023 · Mar 2, 2023
diff --git a/Mathlib/CategoryTheory/Category/Basic.lean b/Mathlib/CategoryTheory/Category/Basic.lean
@@ -37,7 +37,7 @@ I am experimenting with using the `aesop` tactic as a replacement for `tidy`.
 -/
 
 
-library_note "category_theory universes"
+library_note "CategoryTheory universes"
 /--
 The typeclass `Category C` describes morphisms associated to objects of type `C : Type u`.
 

diff --git a/Mathlib/CategoryTheory/Core.lean b/Mathlib/CategoryTheory/Core.lean
@@ -30,7 +30,7 @@ namespace CategoryTheory
 
 universe v₁ v₂ u₁ u₂
 
--- morphism levels before object levels. See note [category_theory universes].
+-- morphism levels before object levels. See note [CategoryTheory universes].
 /-- The core of a category C is the groupoid whose morphisms are all the
 isomorphisms of C. -/
 -- Porting note: This linter does not exist yet

diff --git a/Mathlib/CategoryTheory/EqToHom.lean b/Mathlib/CategoryTheory/EqToHom.lean
@@ -32,7 +32,7 @@ result in the various `eqToHom` morphisms to drop out at the appropriate moment!
 
 universe v₁ v₂ v₃ u₁ u₂ u₃
 
--- morphism levels before object levels. See note [category_theory universes].
+-- morphism levels before object levels. See note [CategoryTheory universes].
 namespace CategoryTheory
 
 open Opposite

diff --git a/Mathlib/CategoryTheory/FullSubcategory.lean b/Mathlib/CategoryTheory/FullSubcategory.lean
@@ -42,7 +42,7 @@ form of `D`. This is used to set up several algebraic categories like
 namespace CategoryTheory
 
 universe v v₂ u₁ u₂
--- morphism levels before object levels. See note [category_theory universes].
+-- morphism levels before object levels. See note [CategoryTheory universes].
 
 section Induced
 

diff --git a/Mathlib/CategoryTheory/Functor/Basic.lean b/Mathlib/CategoryTheory/Functor/Basic.lean
@@ -25,7 +25,7 @@ but in mathlib4 we should switch to this.)
 
 namespace CategoryTheory
 
--- declare the `v`'s first; see note [category_theory universes].
+-- declare the `v`'s first; see note [CategoryTheory universes].
 universe v v₁ v₂ v₃ u u₁ u₂ u₃
 
 section

diff --git a/Mathlib/CategoryTheory/Functor/Category.lean b/Mathlib/CategoryTheory/Functor/Category.lean
@@ -26,7 +26,7 @@ this is a small category at the next higher level.
 
 namespace CategoryTheory
 
--- declare the `v`'s first; see note [category_theory universes].
+-- declare the `v`'s first; see note [CategoryTheory universes].
 universe v₁ v₂ v₃ u₁ u₂ u₃
 
 open NatTrans Category CategoryTheory.Functor

diff --git a/Mathlib/CategoryTheory/Iso.lean b/Mathlib/CategoryTheory/Iso.lean
@@ -39,7 +39,7 @@ category, category theory, isomorphism
 
 universe v u
 
--- morphism levels before object levels. See note [category_theory universes].
+-- morphism levels before object levels. See note [CategoryTheory universes].
 namespace CategoryTheory
 
 open Category

diff --git a/Mathlib/CategoryTheory/NatTrans.lean b/Mathlib/CategoryTheory/NatTrans.lean
@@ -37,7 +37,7 @@ Introduces notations
 
 namespace CategoryTheory
 
--- declare the `v`'s first; see note [category_theory universes].
+-- declare the `v`'s first; see note [CategoryTheory universes].
 universe v₁ v₂ v₃ v₄ u₁ u₂ u₃ u₄
 
 variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]

diff --git a/Mathlib/CategoryTheory/Opposites.lean b/Mathlib/CategoryTheory/Opposites.lean
@@ -30,7 +30,7 @@ set_option autoImplicit false
 
 universe v₁ v₂ u₁ u₂
 
--- morphism levels before object levels. See note [category_theory universes].
+-- morphism levels before object levels. See note [CategoryTheory universes].
 open Opposite
 
 variable {C : Type u₁}

diff --git a/Mathlib/CategoryTheory/Types.lean b/Mathlib/CategoryTheory/Types.lean
@@ -37,7 +37,7 @@ We prove some basic facts about the category `Type`:
 
 namespace CategoryTheory
 
--- morphism levels before object levels. See note [category_theory universes].
+-- morphism levels before object levels. See note [CategoryTheory universes].
 universe v v' w u u'
 
 /- The `@[to_additive]` attribute is just a hint that expressions involving this instance can

diff --git a/Mathlib/Combinatorics/Quiver/Basic.lean b/Mathlib/Combinatorics/Quiver/Basic.lean
@@ -31,7 +31,7 @@ but it is also results in error-prone universe signatures when constraints requi
 open Opposite
 
 -- We use the same universe order as in category theory.
--- See note [category_theory universes]
+-- See note [CategoryTheory universes]
 universe v v₁ v₂ u u₁ u₂
 
 /-- A quiver `G` on a type `V` of vertices assigns to every pair `a b : V` of vertices

diff --git a/Mathlib/Data/Opposite.lean b/Mathlib/Data/Opposite.lean
@@ -21,7 +21,7 @@ category, with all arrows reversed.
 
 universe v u
 
--- morphism levels before object levels. See note [category_theory universes].
+-- morphism levels before object levels. See note [CategoryTheory universes].
 variable (α : Sort u)
 
 /-- The type of objects of the opposite of `α`; used to define the opposite category.