fix(category_theory): simplifying universes (#1122)

Author: kim-em

src/category_theory/adjunction/basic.lean

@@ -13,7 +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 : Sort u₁} [𝒞 : category.{v₁} C] {D : Sort u₂} [𝒟 : category.{v₂} D]
+variables {C : Type u₁} [𝒞 : category.{v₁} C] {D : Type u₂} [𝒟 : category.{v₂} D]
 include 𝒞 𝒟
 
 /--
@@ -172,7 +172,7 @@ def id : functor.id C ⊣ functor.id C :=
 end
 
 section
-variables {E : Sort u₃} [ℰ : category.{v₃} E] (H : D ⥤ E) (I : E ⥤ D)
+variables {E : Type u₃} [ℰ : category.{v₃} E] (H : D ⥤ E) (I : E ⥤ D)
 
 def comp (adj₁ : F ⊣ G) (adj₂ : H ⊣ I) : F ⋙ H ⊣ I ⋙ G :=
 { hom_equiv := λ X Z, equiv.trans (adj₂.hom_equiv _ _) (adj₁.hom_equiv _ _),

src/category_theory/adjunction/limits.lean

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

src/category_theory/category.lean

@@ -31,13 +31,13 @@ powerful tactics.
 def_replacer obviously
 @[obviously] meta def obviously' := tactic.tidy
 
-class has_hom (obj : Sort u) : Sort (max u (v+1)) :=
+class has_hom (obj : Type u) : Type (max u v) :=
 (hom : obj → obj → Sort v)
 
 infixr ` ⟶ `:10 := has_hom.hom -- type as \h
 
-class category_struct (obj : Sort u)
-extends has_hom.{v} obj : Sort (max u (v+1)) :=
+class category_struct (obj : Type u)
+extends has_hom.{v} obj : Type (max u v) :=
 (id       : Π X : obj, hom X X)
 (comp     : Π {X Y Z : obj}, (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z))
 
@@ -49,8 +49,8 @@ The typeclass `category C` describes morphisms associated to objects of type `C`
 The universe levels of the objects and morphisms are unconstrained, and will often need to be
 specified explicitly, as `category.{v} C`. (See also `large_category` and `small_category`.)
 -/
-class category (obj : Sort u)
-extends category_struct.{v} obj : Sort (max u (v+1)) :=
+class category (obj : Type u)
+extends category_struct.{v} obj : Type (max u v) :=
 (id_comp' : ∀ {X Y : obj} (f : hom X Y), 𝟙 X ≫ f = f . obviously)
 (comp_id' : ∀ {X Y : obj} (f : hom X Y), f ≫ 𝟙 Y = f . obviously)
 (assoc'   : ∀ {W X Y Z : obj} (f : hom W X) (g : hom X Y) (h : hom Y Z),
@@ -65,7 +65,7 @@ restate_axiom category.assoc'
 attribute [simp] category.id_comp category.comp_id category.assoc
 attribute [trans] category_struct.comp
 
-lemma category.assoc_symm {C : Sort u} [category.{v} C] {W X Y Z : C} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z) :
+lemma category.assoc_symm {C : Type u} [category.{v} C] {W X Y Z : C} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z) :
   f ≫ (g ≫ h) = (f ≫ g) ≫ h :=
 by rw ←category.assoc
 
@@ -74,14 +74,14 @@ A `large_category` has objects in one universe level higher than the universe le
 the morphisms. It is useful for examples such as the category of types, or the category
 of groups, etc.
 -/
-abbreviation large_category (C : Sort (u+1)) : Sort (u+1) := category.{u} C
+abbreviation large_category (C : Type u) : Type u := category.{u} C
 /--
 A `small_category` has objects and morphisms in the same universe level.
 -/
-abbreviation small_category (C : Sort u)     : Sort (u+1) := category.{u} C
+abbreviation small_category (C : Type u) : Type (u+1) := category.{u+1} C
 
 section
-variables {C : Sort u} [𝒞 : category.{v} C] {X Y Z : C}
+variables {C : Type u} [𝒞 : category.{v} C] {X Y Z : C}
 include 𝒞
 
 lemma eq_of_comp_left_eq {f g : X ⟶ Y} (w : ∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h) : f = g :=

src/category_theory/comma.lean

@@ -8,12 +8,12 @@ import category_theory.punit
 namespace category_theory
 
 universes v₁ v₂ v₃ u₁ u₂ u₃ -- declare the `v`'s first; see `category_theory.category` for an explanation
-variables {A : Sort u₁} [𝒜 : category.{v₁} A]
-variables {B : Sort u₂} [ℬ : category.{v₂} B]
-variables {T : Sort u₃} [𝒯 : category.{v₃} T]
+variables {A : Type u₁} [𝒜 : category.{v₁} A]
+variables {B : Type u₂} [ℬ : category.{v₂} B]
+variables {T : Type u₃} [𝒯 : category.{v₃} T]
 include 𝒜 ℬ 𝒯
 
-structure comma (L : A ⥤ T) (R : B ⥤ T) :=
+structure comma (L : A ⥤ T) (R : B ⥤ T) : Type (max u₁ u₂ v₃) :=
 (left : A . obviously)
 (right : B . obviously)
 (hom : L.obj left ⟶ R.obj right)
@@ -240,7 +240,7 @@ variables {Y : T} {f : X ⟶ Y} {U V : over X} {g : U ⟶ V}
 end
 
 section
-variables {D : Sort u₃} [𝒟 : category.{v₃} D]
+variables {D : Type u₃} [𝒟 : category.{v₃} D]
 include 𝒟
 
 def post (F : T ⥤ D) : over X ⥤ over (F.obj X) :=
@@ -304,7 +304,7 @@ variables {Y : T} {f : X ⟶ Y} {U V : under Y} {g : U ⟶ V}
 end
 
 section
-variables {D : Sort u₃} [𝒟 : category.{v₃} D]
+variables {D : Type u₃} [𝒟 : category.{v₃} D]
 include 𝒟
 
 def post {X : T} (F : T ⥤ D) : under X ⥤ under (F.obj X) :=

src/category_theory/concrete_category.lean

@@ -11,7 +11,7 @@ import category_theory.types
 universes u v
 
 namespace category_theory
-variables {c d : Sort u → Sort v} {α : Sort u}
+variables {c d : Type u → Type v} {α : Type u}
 
 /--
 `concrete_category @hom` collects the evidence that a type constructor `c` and a
@@ -28,23 +28,23 @@ attribute [class] concrete_category
 
 /-- `bundled` is a type bundled with a type class instance for that type. Only
 the type class is exposed as a parameter. -/
-structure bundled (c : Sort u → Sort v) : Sort (max (u+1) v) :=
-(α : Sort u)
+structure bundled (c : Type u → Type v) : Type (max (u+1) v) :=
+(α : Type u)
 (str : c α . tactic.apply_instance)
 
-def mk_ob {c : Sort u → Sort v} (α : Sort u) [str : c α] : bundled c := ⟨α, str⟩
+def mk_ob {c : Type u → Type v} (α : Type u) [str : c α] : bundled c := ⟨α, str⟩
 
 namespace bundled
 
 instance : has_coe_to_sort (bundled c) :=
-{ S := Sort u, coe := bundled.α }
+{ S := Type u, coe := bundled.α }
 
 /-- Map over the bundled structure -/
 def map (f : ∀ {α}, c α → d α) (b : bundled c) : bundled d :=
 ⟨b.α, f b.str⟩
 
 section concrete_category
-variables (hom : ∀ {α β : Sort u}, c α → c β → (α → β) → Prop)
+variables (hom : ∀ {α β : Type u}, c α → c β → (α → β) → Prop)
 variables [h : concrete_category @hom]
 include h
 
@@ -77,21 +77,21 @@ end concrete_category
 end bundled
 
 def concrete_functor
-  {C : Sort u → Sort v} {hC : ∀{α β}, C α → C β → (α → β) → Prop} [concrete_category @hC]
-  {D : Sort u → Sort v} {hD : ∀{α β}, D α → D β → (α → β) → Prop} [concrete_category @hD]
+  {C : Type u → Type v} {hC : ∀{α β}, C α → C β → (α → β) → Prop} [concrete_category @hC]
+  {D : Type u → Type v} {hD : ∀{α β}, D α → D β → (α → β) → Prop} [concrete_category @hD]
   (m : ∀{α}, C α → D α) (h : ∀{α β} {ia : C α} {ib : C β} {f}, hC ia ib f → hD (m ia) (m ib) f) :
   bundled C ⥤ bundled D :=
 { obj := bundled.map @m,
   map := λ X Y f, ⟨ f, h f.2 ⟩ }
 
 section forget
-variables {C : Sort u → Sort v} {hom : ∀α β, C α → C β → (α → β) → Prop} [i : concrete_category hom]
+variables {C : Type u → Type v} {hom : ∀α β, C α → C β → (α → β) → Prop} [i : concrete_category hom]
 include i
 
 /-- The forgetful functor from a bundled category to `Sort`. -/
-def forget : bundled C ⥤ Sort u := { obj := bundled.α, map := λ a b h, h.1 }
+def forget : bundled C ⥤ Type u := { obj := bundled.α, map := λ a b h, h.1 }
 
-instance forget.faithful : faithful (forget : bundled C ⥤ Sort u) :=
+instance forget.faithful : faithful (forget : bundled C ⥤ Type u) :=
 { injectivity' :=
   begin
     rintros X Y ⟨f,_⟩ ⟨g,_⟩ p,

src/category_theory/const.lean

@@ -11,8 +11,8 @@ open category_theory
 
 namespace category_theory.functor
 
-variables (J : Sort u₁) [𝒥 : category.{v₁} J]
-variables {C : Sort u₂} [𝒞 : category.{v₂} C]
+variables (J : Type u₁) [𝒥 : category.{v₁} J]
+variables {C : Type u₂} [𝒞 : category.{v₂} C]
 include 𝒥 𝒞
 
 def const : C ⥤ (J ⥤ C) :=
@@ -52,7 +52,7 @@ end const
 
 
 section
-variables {D : Sort u₃} [𝒟 : category.{v₃} D]
+variables {D : Type u₃} [𝒟 : category.{v₃} D]
 include 𝒟
 
 /-- These are actually equal, of course, but not definitionally equal

src/category_theory/core.lean

@@ -14,9 +14,9 @@ namespace category_theory
 
 universes v₁ v₂ u₁ u₂ -- declare the `v`'s first; see `category_theory.category` for an explanation
 
-def core (C : Sort u₁) := C
+def core (C : Type u₁) := C
 
-variables {C : Sort u₁} [𝒞 : category.{v₁} C]
+variables {C : Type u₁} [𝒞 : category.{v₁} C]
 include 𝒞
 
 instance core_category : groupoid.{(max v₁ 1)} (core C) :=
@@ -34,7 +34,7 @@ def inclusion : core C ⥤ C :=
 { obj := id,
   map := λ X Y f, f.hom }
 
-variables {G : Sort u₂} [𝒢 : groupoid.{v₂} G]
+variables {G : Type u₂} [𝒢 : groupoid.{v₂} G]
 include 𝒢
 
 /-- A functor from a groupoid to a category C factors through the core of C. -/

src/category_theory/discrete_category.lean

@@ -24,7 +24,7 @@ variables {α : Type u₁}
 
 end discrete
 
-variables {C : Sort u₂} [𝒞 : category.{v₂} C]
+variables {C : Type u₂} [𝒞 : category.{v₂} C]
 include 𝒞
 
 namespace functor

src/category_theory/epi_mono.lean

@@ -16,7 +16,7 @@ universes v₁ v₂ u₁ u₂
 
 namespace category_theory
 
-variables {C : Sort u₁} [𝒞 : category.{v₁} C] {D : Sort u₂} [𝒟 : category.{v₂} D]
+variables {C : Type u₁} [𝒞 : category.{v₁} C] {D : Type u₂} [𝒟 : category.{v₂} D]
 include 𝒞 𝒟
 
 lemma left_adjoint_preserves_epi {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G)

src/category_theory/eq_to_hom.lean

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