doc(category_theory): convert comments about universes to library note (

#6748)

docs/tutorial/category_theory/calculating_colimits_in_Top.lean

@@ -82,8 +82,6 @@ pushout.desc (𝟙 _) (𝟙 _) rfl
 
 end Gluing
 
-universes v u w
-
 section Products
 
 /-- The countably infinite product of copies of `ℝ`. -/

docs/tutorial/category_theory/intro.lean

@@ -54,9 +54,7 @@ open category_theory
 
 section category
 
-universes v u  -- the order matters (see below)
-
-variables (C : Type u) [category.{v} C]
+variables (C : Type*) [category C]
 
 variables {W X Y Z : C}
 variables (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z)
@@ -65,13 +63,15 @@ variables (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z)
 This says "let `C` be a category, let `W`, `X`, `Y`, `Z` be objects of `C`, and let `f : W ⟶ X`, `g
 : X ⟶ Y` and `h : Y ⟶ Z` be morphisms in `C` (with the specified source and targets)".
 
-Note that we need to explicitly tell Lean the universe that the morphisms live in, by writing
-`category.{v} C`, because Lean cannot guess this from `C` alone.
+Note that we sometimes need to explicitly tell Lean the universe that the morphisms live in,
+by writing `category.{v} C`, because Lean cannot guess this from `C` alone.
+However just writing `category C` is often fine: this allows a "free" universe level.
 
-The order in which universes are introduced at the top of the file matters: we put the universes for
-morphisms first (typically `v`, `v₁` and so on), and then universes for objects (typically `u`, `u₁`
-and so on). This ensures that in any new definition we make the universe variables for morphisms
-come first, so that they can be explicitly specified while still allowing the universe levels of the
+The order in which universes are introduced at the top of the file matters:
+we put the universes for morphisms first (typically `v`, `v₁` and so on),
+and then universes for objects (typically `u`, `u₁` and so on).
+This ensures that in any new definition we make the universe variables for morphisms come first,
+so that they can be explicitly specified while still allowing the universe levels of the
 objects to be inferred automatically.
 
 ## Basic notation
@@ -122,12 +122,9 @@ functor.
 
 section functor
 
--- recall we put morphism universes (`vᵢ`) before object universes (`uᵢ`)
-universes v₁ v₂ v₃ u₁ u₂ u₃
-
-variables (C : Type u₁) [category.{v₁} C]
-variables (D : Type u₂) [category.{v₂} D]
-variables (E : Type u₃) [category.{v₃} E]
+variables (C : Type*) [category C]
+variables (D : Type*) [category D]
+variables (E : Type*) [category E]
 
 variables {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
 
@@ -180,9 +177,7 @@ use morphism notation for natural transformations.
 
 section nat_trans
 
-universes v₁ v₂ u₁ u₂
-
-variables {C : Type u₁} [category.{v₁} C] {D : Type u₂} [category.{v₂} D]
+variables {C : Type*} [category C] {D : Type*} [category D]
 
 variables (X Y : C)
 

src/category_theory/adjunction/opposites.lean

@@ -22,7 +22,7 @@ adjunction, opposite, uniqueness
 
 open category_theory
 
-universes v₁ v₂ u₁ u₂ -- declare the `v`'s first; see `category_theory.category` for an explanation
+universes v₁ v₂ u₁ u₂ -- morphism levels before object levels. See note [category_theory universes].
 
 variables {C : Type u₁} [category.{v₁} C] {D : Type u₂} [category.{v₂} D]
 

src/category_theory/arrow.lean

@@ -22,7 +22,7 @@ comma, arrow
 
 namespace category_theory
 
-universes v u -- declare the `v`'s first; see `category_theory.category` for an explanation
+universes v u -- morphism levels before object levels. See note [category_theory universes].
 variables {T : Type u} [category.{v} T]
 
 section

src/category_theory/category/default.lean

@@ -22,8 +22,51 @@ local notation f ` ⊚ `:80 g:80 := category.comp g f    -- type as \oo
 ```
 -/
 
--- The order in this declaration matters: v often needs to be explicitly specified while u often
--- can be omitted
+/--
+The typeclass `category C` describes morphisms associated to objects of type `C : Type u`.
+
+The universe levels of the objects and morphisms are independent, and will often need to be
+specified explicitly, as `category.{v} C`.
+
+Typically any concrete example will either be a `small_category`, where `v = u`,
+which can be introduced as
+```
+universes u
+variables {C : Type u} [small_category C]
+```
+or a `large_category`, where `u = v+1`, which can be introduced as
+```
+universes u
+variables {C : Type (u+1)} [large_category C]
+```
+
+In order for the library to handle these cases uniformly,
+we generally work with the unconstrained `category.{v u}`,
+for which objects live in `Type u` and morphisms live in `Type v`.
+
+Because the universe parameter `u` for the objects can be inferred from `C`
+when we write `category C`, while the universe parameter `v` for the morphisms
+can not be automatically inferred, through the category theory library
+we introduce universe parameters with morphism levels listed first,
+as in
+```
+universes v u
+```
+or
+```
+universes v₁ v₂ u₁ u₂
+```
+when multiple independent universes are needed.
+
+This has the effect that we can simply write `category.{v} C`
+(that is, only specifying a single parameter) while `u` will be inferred.
+
+Often, however, it's not even necessary to include the `.{v}`.
+(Although it was in earlier versions of Lean.)
+If it is omitted a "free" universe will be used.
+-/
+library_note "category_theory universes"
+
 universes v u
 
 namespace category_theory

src/category_theory/core.lean

@@ -9,7 +9,7 @@ import category_theory.types
 
 namespace category_theory
 
-universes v₁ v₂ u₁ u₂ -- declare the `v`'s first; see `category_theory.category` for an explanation
+universes v₁ v₂ u₁ u₂ -- morphism levels before object levels. See note [category_theory universes].
 
 /-- The core of a category C is the groupoid whose morphisms are all the
 isomorphisms of C. -/

src/category_theory/discrete_category.lean

@@ -7,7 +7,7 @@ import category_theory.eq_to_hom
 
 namespace category_theory
 
-universes v₁ v₂ u₁ u₂ -- declare the `v`'s first; see `category_theory.category` for an explanation
+universes v₁ v₂ u₁ u₂ -- morphism levels before object levels. See note [category_theory universes].
 
 /--
 A type synonym for promoting any type to a category,

src/category_theory/eq_to_hom.lean

@@ -5,7 +5,7 @@ Authors: Reid Barton, Scott Morrison
 -/
 import category_theory.opposites
 
-universes v₁ v₂ u₁ u₂ -- declare the `v`'s first; see `category_theory.category` for an explanation
+universes v₁ v₂ u₁ u₂ -- morphism levels before object levels. See note [category_theory universes].
 
 namespace category_theory
 open opposite

src/category_theory/full_subcategory.lean

@@ -7,7 +7,7 @@ import category_theory.fully_faithful
 
 namespace category_theory
 
-universes v u₁ u₂ -- declare the `v`'s first; see `category_theory.category` for an explanation
+universes v u₁ u₂ -- morphism levels before object levels. See note [category_theory universes].
 
 section induced
 

src/category_theory/groupoid.lean

@@ -7,7 +7,7 @@ import category_theory.epi_mono
 
 namespace category_theory
 
-universes v v₂ u u₂ -- declare the `v`'s first; see `category_theory.category` for an explanation
+universes v v₂ u u₂ -- morphism levels before object levels. See note [category_theory universes].
 
 /-- A `groupoid` is a category such that all morphisms are isomorphisms. -/
 class groupoid (obj : Type u) extends category.{v} obj : Type (max u (v+1)) :=

src/category_theory/isomorphism.lean

@@ -31,7 +31,7 @@ This file defines isomorphisms between objects of a category.
 category, category theory, isomorphism
 -/
 
-universes v u -- declare the `v`'s first; see `category_theory.category` for an explanation
+universes v u -- morphism levels before object levels. See note [category_theory universes].
 
 namespace category_theory
 open category

src/category_theory/limits/cones.lean

@@ -8,7 +8,7 @@ import category_theory.discrete_category
 import category_theory.yoneda
 import category_theory.reflects_isomorphisms
 
-universes v u u' -- declare the `v`'s first; see `category_theory.category` for an explanation
+universes v u u' -- morphism levels before object levels. See note [category_theory universes].
 
 open category_theory
 

src/category_theory/limits/constructions/over/connected.lean

@@ -14,7 +14,7 @@ Shows that the forgetful functor `over B ⥤ C` creates connected limits, in par
 any connected limit which `C` has.
 -/
 
-universes v u -- declare the `v`'s first; see `category_theory.category` for an explanation
+universes v u -- morphism levels before object levels. See note [category_theory universes].
 
 noncomputable theory
 

src/category_theory/limits/constructions/over/default.lean

@@ -14,7 +14,7 @@ import category_theory.limits.constructions.equalizers
 Declare instances for limits in the over category: If `C` has finite wide pullbacks, `over B` has
 finite limits, and if `C` has arbitrary wide pullbacks then `over B` has limits.
 -/
-universes v u -- declare the `v`'s first; see `category_theory.category` for an explanation
+universes v u -- morphism levels before object levels. See note [category_theory universes].
 
 open category_theory category_theory.limits
 

src/category_theory/limits/constructions/over/products.lean

@@ -15,7 +15,7 @@ Shows that products in the over category can be derived from wide pullbacks in t
 The main result is `over_product_of_wide_pullback`, which says that if `C` has `J`-indexed wide
 pullbacks, then `over B` has `J`-indexed products.
 -/
-universes v u -- declare the `v`'s first; see `category_theory.category` for an explanation
+universes v u -- morphism levels before object levels. See note [category_theory universes].
 
 open category_theory category_theory.limits
 

src/category_theory/limits/functor_category.lean

@@ -9,7 +9,7 @@ open category_theory category_theory.category
 
 namespace category_theory.limits
 
-universes v v₂ u -- declare the `v`'s first; see `category_theory.category` for an explanation
+universes v v₂ u -- morphism levels before object levels. See note [category_theory universes].
 
 variables {C : Type u} [category.{v} C]
 

src/category_theory/limits/limits.lean

@@ -66,7 +66,8 @@ open category_theory category_theory.category category_theory.functor opposite
 
 namespace category_theory.limits
 
-universes v u u' u'' w -- declare the `v`'s first; see `category_theory.category` for an explanation
+-- morphism levels before object levels. See note [category_theory universes].
+universes v u u' u'' w
 
 variables {J K : Type v} [small_category J] [small_category K]
 variables {C : Type u} [category.{v} C]

src/category_theory/limits/over.lean

@@ -23,7 +23,7 @@ TODO: If `C` has binary products, then `forget X : over X ⥤ C` has a right adj
 -/
 noncomputable theory
 
-universes v u -- declare the `v`'s first; see `category_theory.category` for an explanation
+universes v u -- morphism levels before object levels. See note [category_theory universes].
 
 open category_theory category_theory.limits
 

src/category_theory/limits/preserves/basic.lean

@@ -38,7 +38,7 @@ noncomputable theory
 
 namespace category_theory.limits
 
-universes v u₁ u₂ u₃ -- declare the `v`'s first; see `category_theory.category` for an explanation
+universes v u₁ u₂ u₃ -- morphism levels before object levels. See note [category_theory universes].
 
 variables {C : Type u₁} [category.{v} C]
 variables {D : Type u₂} [category.{v} D]

src/category_theory/monad/adjunction.lean

@@ -9,7 +9,7 @@ import category_theory.adjunction
 namespace category_theory
 open category
 
-universes v₁ v₂ u₁ u₂ -- declare the `v`'s first; see `category_theory.category` for an explanation
+universes v₁ v₂ u₁ u₂ -- morphism levels before object levels. See note [category_theory universes].
 
 variables {C : Type u₁} [category.{v₁} C] {D : Type u₂} [category.{v₂} D]
 variables (L : C ⥤ D) (R : D ⥤ C)

src/category_theory/monad/algebra.lean

@@ -24,7 +24,7 @@ cofree functors, respectively from and to the original category.
 namespace category_theory
 open category
 
-universes v₁ u₁ -- declare the `v`'s first; see `category_theory.category` for an explanation
+universes v₁ u₁ -- morphism levels before object levels. See note [category_theory universes].
 
 variables {C : Type u₁} [category.{v₁} C]
 

src/category_theory/monad/basic.lean

@@ -9,7 +9,7 @@ import category_theory.fully_faithful
 namespace category_theory
 open category
 
-universes v₁ u₁ -- declare the `v`'s first; see `category_theory.category` for an explanation
+universes v₁ u₁ -- morphism levels before object levels. See note [category_theory universes].
 
 variables (C : Type u₁) [category.{v₁} C]
 

src/category_theory/monad/bundled.lean

@@ -20,7 +20,7 @@ in the sense of `category_theory.(co)monad_hom`. We construct a category instanc
 namespace category_theory
 open category
 
-universes v u -- declare the `v`'s first; see `category_theory.category` for an explanation
+universes v u -- morphism levels before object levels. See note [category_theory universes].
 
 variables (C : Type u) [category.{v} C]
 

src/category_theory/monad/equiv_mon.lean

@@ -26,7 +26,7 @@ A monad "is just" a monoid in the category of endofunctors.
 namespace category_theory
 open category
 
-universes v u -- declare the `v`'s first; see `category_theory.category` for an explanation
+universes v u -- morphism levels before object levels. See note [category_theory universes].
 variables {C : Type u} [category.{v} C]
 
 namespace Monad

src/category_theory/monad/kleisli.lean

@@ -18,7 +18,7 @@ adjunction which gives rise to the monad `(T, η_ T, μ_ T)`.
 -/
 namespace category_theory
 
-universes v u -- declare the `v`'s first; see `category_theory.category` for an explanation
+universes v u -- morphism levels before object levels. See note [category_theory universes].
 
 variables {C : Type u} [category.{v} C]
 

src/category_theory/monad/limits.lean

@@ -11,7 +11,7 @@ namespace category_theory
 open category
 open category_theory.limits
 
-universes v₁ v₂ u₁ u₂ -- declare the `v`'s first; see `category_theory.category` for an explanation
+universes v₁ v₂ u₁ u₂ -- morphism levels before object levels. See note [category_theory universes].
 
 namespace monad
 

src/category_theory/monad/products.lean

@@ -24,7 +24,7 @@ is a monadic right adjoint.
 
 noncomputable theory
 
-universes v u -- declare the `v`'s first; see `category_theory.category` for an explanation
+universes v u -- morphism levels before object levels. See note [category_theory universes].
 
 namespace category_theory
 open category limits

src/category_theory/opposites.lean

@@ -7,7 +7,7 @@ import category_theory.types
 import category_theory.equivalence
 import data.opposite
 
-universes v₁ v₂ u₁ u₂ -- declare the `v`'s first; see `category_theory.category` for an explanation
+universes v₁ v₂ u₁ u₂ -- morphism levels before object levels. See note [category_theory universes].
 
 namespace category_theory
 open opposite

src/category_theory/over.lean

@@ -24,7 +24,7 @@ comma, slice, coslice, over, under
 
 namespace category_theory
 
-universes v₁ v₂ u₁ u₂ -- declare the `v`'s first; see `category_theory.category` for an explanation
+universes v₁ v₂ u₁ u₂ -- morphism levels before object levels. See note [category_theory universes].
 variables {T : Type u₁} [category.{v₁} T]
 
 /--

src/category_theory/pempty.lean

@@ -11,7 +11,7 @@ import category_theory.discrete_category
 Defines a category structure on `pempty`, and the unique functor `pempty ⥤ C` for any category `C`.
 -/
 
-universes v u w -- declare the `v`'s first; see `category_theory.category` for an explanation
+universes v u w -- morphism levels before object levels. See note [category_theory universes].
 
 namespace category_theory
 namespace functor

src/category_theory/punit.lean

@@ -6,7 +6,7 @@ Authors: Scott Morrison, Bhavik Mehta
 import category_theory.const
 import category_theory.discrete_category
 
-universes v u -- declare the `v`'s first; see `category_theory.category` for an explanation
+universes v u -- morphism levels before object levels. See note [category_theory universes].
 
 namespace category_theory
 

src/category_theory/sums/basic.lean

@@ -11,7 +11,7 @@ Disjoint unions of categories, functors, and natural transformations.
 
 namespace category_theory
 
-universes v₁ u₁ -- declare the `v`'s first; see `category_theory.category` for an explanation
+universes v₁ u₁ -- morphism levels before object levels. See note [category_theory universes].
 
 open sum
 

src/category_theory/types.lean

@@ -31,7 +31,8 @@ We prove some basic facts about the category `Type`:
 
 namespace category_theory
 
-universes v v' w u u' -- declare the `v`'s first; see `category_theory.category` for an explanation
+-- morphism levels before object levels. See note [category_theory universes].
+universes v v' w u u'
 
 instance types : large_category (Type u) :=
 { hom     := λ a b, (a → b),