feat(category_theory): working in Sort rather than Type (#824)

Author: kim-em

src/category_theory/adjunction.lean

@@ -16,7 +16,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]
+variables {C : Sort u₁} [𝒞 : category.{v₁} C] {D : Sort u₂} [𝒟 : category.{v₂} D]
 include 𝒞 𝒟
 
 /--
@@ -179,7 +179,7 @@ TODO
 -/
 
 section
-variables {E : Type u₃} [ℰ : category.{v₃} E] (H : D ⥤ E) (I : E ⥤ D)
+variables {E : Sort u₃} [ℰ : category.{v₃} E] (H : D ⥤ E) (I : E ⥤ D)
 
 def comp (adj₁ : adjunction F G) (adj₂ : adjunction H I) : adjunction (F ⋙ H) (I ⋙ G) :=
 { hom_equiv := λ X Z, equiv.trans (adj₂.hom_equiv _ _) (adj₁.hom_equiv _ _),
@@ -275,7 +275,7 @@ open category_theory.limits
 
 universes u₁ u₂ v
 
-variables {C : Type u₁} [𝒞 : category.{v} C] {D : Type u₂} [𝒟 : category.{v} D]
+variables {C : Sort u₁} [𝒞 : category.{v+1} C] {D : Sort u₂} [𝒟 : category.{v+1} D]
 include 𝒞 𝒟
 
 variables {F : C ⥤ D} {G : D ⥤ C} (adj : adjunction F G)

src/category_theory/category.lean

@@ -33,13 +33,13 @@ powerful tactics.
 def_replacer obviously
 @[obviously] meta def obviously' := tactic.tidy
 
-class has_hom (obj : Type u) : Type (max u (v+1)) :=
-(hom : obj → obj → Type v)
+class has_hom (obj : Sort u) : Sort (max u (v+1)) :=
+(hom : obj → obj → Sort v)
 
 infixr ` ⟶ `:10 := has_hom.hom -- type as \h
 
-class category_struct (obj : Type u)
-extends has_hom.{v} obj :=
+class category_struct (obj : Sort u)
+extends has_hom.{v} obj : Sort (max u (v+1)) :=
 (id       : Π X : obj, hom X X)
 (comp     : Π {X Y Z : obj}, (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z))
 
@@ -51,8 +51,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 : Type u)
-extends category_struct.{v} obj :=
+class category (obj : Sort u)
+extends category_struct.{v} obj : Sort (max u (v+1)) :=
 (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),
@@ -76,14 +76,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 : Type (u+1)) : Type (u+1) := category.{u} C
+abbreviation large_category (C : Sort (u+1)) : Sort (u+1) := category.{u} C
 /--
 A `small_category` has objects and morphisms in the same universe level.
 -/
-abbreviation small_category (C : Type u)     : Type (u+1) := category.{u} C
+abbreviation small_category (C : Sort u)     : Sort (u+1) := category.{u} C
 
 section
-variables {C : Type u} [𝒞 : category.{v} C] {X Y Z : C}
+variables {C : Sort u} [𝒞 : category.{v} C] {X Y Z : C}
 include 𝒞
 
 class epi  (f : X ⟶ Y) : Prop :=
@@ -124,14 +124,14 @@ variables {C : Type u}
 
 def End [has_hom.{v} C] (X : C) := X ⟶ X
 
-instance End.has_one [category_struct.{v} C] {X : C} : has_one (End X) := by refine { one := 𝟙 X }
-instance End.has_mul [category_struct.{v} C] {X : C} : has_mul (End X) := by refine { mul := λ x y, x ≫ y }
-instance End.monoid [category.{v} C] {X : C} : monoid (End X) :=
+instance End.has_one [category_struct.{v+1} C] {X : C} : has_one (End X) := by refine { one := 𝟙 X }
+instance End.has_mul [category_struct.{v+1} C] {X : C} : has_mul (End X) := by refine { mul := λ x y, x ≫ y }
+instance End.monoid [category.{v+1} C] {X : C} : monoid (End X) :=
 by refine { .. End.has_one, .. End.has_mul, .. }; dsimp [has_mul.mul,has_one.one]; obviously
 
-@[simp] lemma End.one_def {C : Type u} [category_struct.{v} C] {X : C} : (1 : End X) = 𝟙 X := rfl
+@[simp] lemma End.one_def {C : Type u} [category_struct.{v+1} C] {X : C} : (1 : End X) = 𝟙 X := rfl
 
-@[simp] lemma End.mul_def {C : Type u} [category_struct.{v} C] {X : C} (xs ys : End X) : xs * ys = xs ≫ ys := rfl
+@[simp] lemma End.mul_def {C : Type u} [category_struct.{v+1} C] {X : C} (xs ys : End X) : xs * ys = xs ≫ ys := rfl
 
 end
 

src/category_theory/comma.lean

@@ -12,9 +12,9 @@ import category_theory.equivalence
 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]
+variables {A : Sort u₁} [𝒜 : category.{v₁} A]
+variables {B : Sort u₂} [ℬ : category.{v₂} B]
+variables {T : Sort u₃} [𝒯 : category.{v₃} T]
 include 𝒜 ℬ 𝒯
 
 structure comma (L : A ⥤ T) (R : B ⥤ T) :=
@@ -193,7 +193,7 @@ end comma
 
 omit 𝒜 ℬ
 
-def over (X : T) := comma.{v₃ 0 v₃} (functor.id T) (functor.of.obj X)
+def over (X : T) := comma.{v₃ 1 v₃} (functor.id T) (functor.of.obj X)
 
 namespace over
 
@@ -244,8 +244,8 @@ variables {Y : T} {f : X ⟶ Y} {U V : over X} {g : U ⟶ V}
 end
 
 section
-variables {D : Type u₃} [Dcat : category.{v₃} D]
-include Dcat
+variables {D : Sort u₃} [𝒟 : category.{v₃} D]
+include 𝒟
 
 def post (F : T ⥤ D) : over X ⥤ over (F.obj X) :=
 { obj := λ Y, mk $ F.map Y.hom,
@@ -257,7 +257,7 @@ end
 
 end over
 
-def under (X : T) := comma.{0 v₃ v₃} (functor.of.obj X) (functor.id T)
+def under (X : T) := comma.{1 v₃ v₃} (functor.of.obj X) (functor.id T)
 
 namespace under
 
@@ -308,8 +308,8 @@ variables {Y : T} {f : X ⟶ Y} {U V : under Y} {g : U ⟶ V}
 end
 
 section
-variables {D : Type u₃} [Dcat : category.{v₃} D]
-include Dcat
+variables {D : Sort u₃} [𝒟 : category.{v₃} D]
+include 𝒟
 
 def post {X : T} (F : T ⥤ D) : under X ⥤ under (F.obj X) :=
 { obj := λ Y, mk $ F.map Y.hom,

src/category_theory/concrete_category.lean

@@ -11,7 +11,7 @@ import category_theory.types
 universes u v
 
 namespace category_theory
-variables {c d : Type u → Type v} {α : Type u}
+variables {c d : Sort u → Sort v} {α : Sort 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 : Type u → Type v) : Type (max (u+1) v) :=
-(α : Type u)
+structure bundled (c : Sort u → Sort v) : Sort (max (u+1) v) :=
+(α : Sort u)
 (str : c α)
 
-def mk_ob {c : Type u → Type v} (α : Type u) [str : c α] : bundled c := ⟨α, str⟩
+def mk_ob {c : Sort u → Sort v} (α : Sort u) [str : c α] : bundled c := ⟨α, str⟩
 
 namespace bundled
 
 instance : has_coe_to_sort (bundled c) :=
-{ S := Type u, coe := bundled.α }
+{ S := Sort 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 : ∀ {α β : Type u}, c α → c β → (α → β) → Prop)
+variables (hom : ∀ {α β : Sort u}, c α → c β → (α → β) → Prop)
 variables [h : concrete_category @hom]
 include h
 
@@ -74,21 +74,26 @@ end concrete_category
 end bundled
 
 def concrete_functor
-  {C : Type u → Type v} {hC : ∀{α β}, C α → C β → (α → β) → Prop} [concrete_category @hC]
-  {D : Type u → Type v} {hD : ∀{α β}, D α → D β → (α → β) → Prop} [concrete_category @hD]
+  {C : Sort u → Sort v} {hC : ∀{α β}, C α → C β → (α → β) → Prop} [concrete_category @hC]
+  {D : Sort u → Sort 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 ⟩}
+  map := λ X Y f, ⟨ f, h f.2 ⟩ }
 
 section forget
-variables {C : Type u → Type v} {hom : ∀α β, C α → C β → (α → β) → Prop} [i : concrete_category hom]
+variables {C : Sort u → Sort v} {hom : ∀α β, C α → C β → (α → β) → Prop} [i : concrete_category hom]
 include i
 
-/-- The forgetful functor from a bundled category to `Type`. -/
-def forget : bundled C ⥤ Type u := { obj := bundled.α, map := λa b h, h.1 }
+/-- The forgetful functor from a bundled category to `Sort`. -/
+def forget : bundled C ⥤ Sort u := { obj := bundled.α, map := λ a b h, h.1 }
 
-instance forget.faithful : faithful (forget : bundled C ⥤ Type u) := {}
+instance forget.faithful : faithful (forget : bundled C ⥤ Sort u) :=
+{ injectivity' :=
+  begin
+    rintros X Y ⟨f,_⟩ ⟨g,_⟩ p,
+    congr, exact p,
+  end }
 
 end forget
 

src/category_theory/const.lean

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

src/category_theory/discrete_category.lean

@@ -11,14 +11,15 @@ namespace category_theory
 
 universes v₁ v₂ u₁ u₂ -- declare the `v`'s first; see `category_theory.category` for an explanation
 
+-- We only work in `Type`, rather than `Sort`, as we need to use `ulift`.
 def discrete (α : Type u₁) := α
 
 instance discrete_category (α : Type u₁) : small_category (discrete α) :=
 { hom  := λ X Y, ulift (plift (X = Y)),
   id   := by tidy,
   comp := by tidy }
 
-variables {C : Type u₂} [𝒞 : category.{v₂} C]
+variables {C : Sort u₂} [𝒞 : category.{v₂} C]
 include 𝒞
 
 namespace functor

src/category_theory/eq_to_hom.lean

@@ -9,7 +9,7 @@ universes v v' u u' -- declare the `v`'s first; see `category_theory.category` f
 
 namespace category_theory
 
-variables {C : Type u} [𝒞 : category.{v} C]
+variables {C : Sort u} [𝒞 : category.{v} C]
 include 𝒞
 
 def eq_to_hom {X Y : C} (p : X = Y) : X ⟶ Y := by rw p; exact 𝟙 _
@@ -33,7 +33,7 @@ rfl
   eq_to_iso p ≪≫ eq_to_iso q = eq_to_iso (p.trans q) :=
 by ext; simp
 
-variables {D : Type u'} [𝒟 : category.{v'} D]
+variables {D : Sort u'} [𝒟 : category.{v'} D]
 include 𝒟
 
 namespace functor

src/category_theory/equivalence.lean

@@ -12,7 +12,7 @@ namespace category_theory
 
 universes v₁ v₂ v₃ u₁ u₂ u₃ -- declare the `v`'s first; see `category_theory.category` for an explanation
 
-structure equivalence (C : Type u₁) [category.{v₁} C] (D : Type u₂) [category.{v₂} D] :=
+structure equivalence (C : Sort u₁) [category.{v₁} C] (D : Sort u₂) [category.{v₂} D] :=
 (functor : C ⥤ D)
 (inverse : D ⥤ C)
 (fun_inv_id' : (functor ⋙ inverse) ≅ (category_theory.functor.id C) . obviously)
@@ -25,14 +25,14 @@ infixr ` ≌ `:10  := equivalence
 
 namespace equivalence
 
-variables {C : Type u₁} [𝒞 : category.{v₁} C]
+variables {C : Sort u₁} [𝒞 : category.{v₁} C]
 include 𝒞
 
 @[refl] def refl : C ≌ C :=
 { functor := functor.id C,
   inverse := functor.id C }
 
-variables {D : Type u₂} [𝒟 : category.{v₂} D]
+variables {D : Sort u₂} [𝒟 : category.{v₂} D]
 include 𝒟
 
 @[symm] def symm (e : C ≌ D) : D ≌ C :=
@@ -54,7 +54,7 @@ begin
   refl
 end
 
-variables {E : Type u₃} [ℰ : category.{v₃} E]
+variables {E : Sort u₃} [ℰ : category.{v₃} E]
 include ℰ
 
 @[simp] private def effe_iso_id (e : C ≌ D) (f : D ≌ E) (X : C) :
@@ -94,11 +94,11 @@ calc
 
 end equivalence
 
-variables {C : Type u₁} [𝒞 : category.{v₁} C]
+variables {C : Sort u₁} [𝒞 : category.{v₁} C]
 include 𝒞
 
 section
-variables {D : Type u₂} [𝒟 : category.{v₂} D]
+variables {D : Sort u₂} [𝒟 : category.{v₂} D]
 include 𝒟
 
 class is_equivalence (F : C ⥤ D) :=
@@ -111,7 +111,7 @@ restate_axiom is_equivalence.inv_fun_id'
 end
 
 namespace is_equivalence
-variables {D : Type u₂} [𝒟 : category.{v₂} D]
+variables {D : Sort u₂} [𝒟 : category.{v₂} D]
 include 𝒟
 
 instance of_equivalence (F : C ≌ D) : is_equivalence (F.functor) :=
@@ -129,7 +129,7 @@ instance is_equivalence_refl : is_equivalence (functor.id C) :=
 { inverse := functor.id C }
 end functor
 
-variables {D : Type u₂} [𝒟 : category.{v₂} D]
+variables {D : Sort u₂} [𝒟 : category.{v₂} D]
 include 𝒟
 
 namespace functor
@@ -153,7 +153,7 @@ def as_equivalence (F : C ⥤ D) [is_equivalence F] : C ≌ D :=
   fun_inv_id' := is_equivalence.fun_inv_id F,
   inv_fun_id' := is_equivalence.inv_fun_id F }
 
-variables {E : Type u₃} [ℰ : category.{v₃} E]
+variables {E : Sort u₃} [ℰ : category.{v₃} E]
 include ℰ
 
 instance is_equivalence_trans (F : C ⥤ D) (G : D ⥤ E) [is_equivalence F] [is_equivalence G] :

src/category_theory/full_subcategory.lean

@@ -24,12 +24,12 @@ section induced
 
 -/
 
-variables {C : Type u₁} {D : Type u₂} [𝒟 : category.{v u₂} D]
+variables {C : Sort u₁} {D : Sort u₂} [𝒟 : category.{v u₂} D]
 include 𝒟
 variables (F : C → D)
 include F
 
-def induced_category : Type u₁ := C
+def induced_category : Sort u₁ := C
 
 instance induced_category.category : category.{v} (induced_category F) :=
 { hom  := λ X Y, F X ⟶ F Y,
@@ -50,7 +50,7 @@ end induced
 section full_subcategory
 /- A full subcategory is the special case of an induced category with F = subtype.val. -/
 
-variables {C : Type u₂} [𝒞 : category.{v} C]
+variables {C : Sort u₂} [𝒞 : category.{v} C]
 include 𝒞
 variables (Z : C → Prop)