fix(category_theory): require morphisms are in Type, again (#1412)

* chore(category_theory): require morphisms live in Type

* move back to Type

* fixes

src/algebraic_geometry/presheafed_space.lean

@@ -23,7 +23,7 @@ open topological_space
 open opposite
 open category_theory.category category_theory.functor
 
-variables (C : Type u) [𝒞 : category.{v+1} C]
+variables (C : Type u) [𝒞 : category.{v} C]
 include 𝒞
 
 local attribute [tidy] tactic.op_induction'
@@ -67,7 +67,7 @@ end
 
 def id (X : PresheafedSpace.{v} C) : hom X X :=
 { f := 𝟙 (X : Top.{v}),
-  c := ((functor.left_unitor _).inv) ≫ (whisker_right (nat_trans.op (opens.map_id _).hom) _) }
+  c := ((functor.left_unitor _).inv) ≫ (whisker_right (nat_trans.op (opens.map_id (X.to_Top)).hom) _) }
 
 def comp (X Y Z : PresheafedSpace.{v} C) (α : hom X Y) (β : hom Y Z) : hom X Z :=
 { f := α.f ≫ β.f,
@@ -131,7 +131,7 @@ instance {X Y : PresheafedSpace.{v} C} : has_coe (X ⟶ Y) (X.to_Top ⟶ Y.to_To
 
 lemma id_c (X : PresheafedSpace.{v} C) :
   ((𝟙 X) : X ⟶ X).c =
-  (((functor.left_unitor _).inv) ≫ (whisker_right (nat_trans.op (opens.map_id _).hom) _)) := rfl
+  (((functor.left_unitor _).inv) ≫ (whisker_right (nat_trans.op (opens.map_id (X.to_Top)).hom) _)) := rfl
 
 -- Implementation note: this harmless looking lemma causes deterministic timeouts,
 -- but happily we can survive without it.
@@ -160,7 +160,7 @@ variables {C}
 
 namespace category_theory
 
-variables {D : Type u} [𝒟 : category.{v+1} D]
+variables {D : Type u} [𝒟 : category.{v} D]
 include 𝒟
 
 local attribute [simp] presheaf.pushforward
@@ -209,7 +209,7 @@ def on_presheaf {F G : C ⥤ D} (α : F ⟶ G) : G.map_presheaf ⟶ F.map_preshe
 { app := λ X,
   { f := 𝟙 _,
     c := whisker_left X.𝒪 α ≫ ((functor.left_unitor _).inv) ≫
-           (whisker_right (nat_trans.op (opens.map_id _).hom) _) },
+           (whisker_right (nat_trans.op (opens.map_id X.to_Top).hom) _) },
   naturality' := λ X Y f,
   begin
     ext1, swap,

src/algebraic_geometry/stalks.lean

@@ -20,7 +20,7 @@ open category_theory.limits category_theory.category category_theory.functor
 open algebraic_geometry
 open topological_space
 
-variables {C : Type u} [𝒞 : category.{v+1} C] [has_colimits.{v} C]
+variables {C : Type u} [𝒞 : category.{v} C] [has_colimits.{v} C]
 include 𝒞
 
 local attribute [tidy] tactic.op_induction'

src/category_theory/adjunction/limits.lean

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

src/category_theory/category/Cat.lean

@@ -33,7 +33,7 @@ instance str (C : Cat.{v u}) : category.{v u} C.α := C.str
 def of (C : Type u) [category.{v} C] : Cat.{v u} := mk_ob C
 
 /-- Category structure on `Cat` -/
-instance category : category.{(max u v)+1 (max v (u+1))} Cat.{v u} :=
+instance category : large_category.{max v u} Cat.{v u} :=
 { hom := λ C D, C.α ⥤ D.α,
   id := λ C, 𝟭 C.α,
   comp := λ C D E F G, F ⋙ G,

src/category_theory/category/Groupoid.lean

@@ -36,7 +36,7 @@ instance str (C : Groupoid.{v u}) : groupoid.{v u} C.α := C.str
 def of (C : Type u) [groupoid.{v} C] : Groupoid.{v u} := mk_ob C
 
 /-- Category structure on `Groupoid` -/
-instance category : category.{(max u v)+1 (max v (u+1))} Groupoid.{v u} :=
+instance category : large_category.{max v u} Groupoid.{v u} :=
 { hom := λ C D, C.α ⥤ D.α,
   id := λ C, 𝟭 C.α,
   comp := λ C D E F G, F ⋙ G,

src/category_theory/category/default.lean

@@ -31,13 +31,13 @@ powerful tactics.
 def_replacer obviously
 @[obviously] meta def obviously' := tactic.tidy
 
-class has_hom (obj : Type u) : Type (max u v) :=
-(hom : obj → obj → Sort v)
+class has_hom (obj : Type u) : Type (max u (v+1)) :=
+(hom : obj → obj → Type v)
 
 infixr ` ⟶ `:10 := has_hom.hom -- type as \h
 
 class category_struct (obj : Type u)
-extends has_hom.{v} obj : Type (max u v) :=
+extends has_hom.{v} obj : Type (max u (v+1)) :=
 (id       : Π X : obj, hom X X)
 (comp     : Π {X Y Z : obj}, (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z))
 
@@ -50,7 +50,7 @@ The universe levels of the objects and morphisms are unconstrained, and will oft
 specified explicitly, as `category.{v} C`. (See also `large_category` and `small_category`.)
 -/
 class category (obj : Type u)
-extends category_struct.{v} obj : Type (max u v) :=
+extends category_struct.{v} obj : Type (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),
@@ -74,11 +74,11 @@ 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) : Type u := category.{u} C
+abbreviation large_category (C : Type (u+1)) : Type (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+1} C
+abbreviation small_category (C : Type u) : Type (u+1) := category.{u} C
 
 section
 variables {C : Type u} [𝒞 : category.{v} C] {X Y Z : C}

src/category_theory/comma.lean

@@ -190,7 +190,7 @@ end comma
 
 omit 𝒜 ℬ
 
-def over (X : T) := comma.{v₃ 1 v₃} (𝟭 T) (functor.of.obj X)
+def over (X : T) := comma.{v₃ 0 v₃} (𝟭 T) (functor.of.obj X)
 
 namespace over
 
@@ -254,7 +254,7 @@ end
 
 end over
 
-def under (X : T) := comma.{1 v₃ v₃} (functor.of.obj X) (𝟭 T)
+def under (X : T) := comma.{0 v₃ v₃} (functor.of.obj X) (𝟭 T)
 
 namespace under
 

src/category_theory/conj.lean

@@ -22,7 +22,7 @@ namespace category_theory
 
 namespace iso
 
-variables {C : Type u} [𝒞 : category.{v+1} C]
+variables {C : Type u} [𝒞 : category.{v} C]
 include 𝒞
 
 /- If `X` is isomorphic to `X₁` and `Y` is isomorphic to `Y₁`, then
@@ -122,7 +122,7 @@ namespace functor
 
 universes v₁ u₁
 
-variables {C : Type u} [𝒞 : category.{v+1} C] {D : Type u₁} [𝒟 : category.{v₁+1} D] (F : C ⥤ D)
+variables {C : Type u} [𝒞 : category.{v} C] {D : Type u₁} [𝒟 : category.{v₁} D] (F : C ⥤ D)
 include 𝒞 𝒟
 
 lemma map_hom_congr {X Y X₁ Y₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (f : X ⟶ Y) :

src/category_theory/core.lean

@@ -19,7 +19,7 @@ def core (C : Type u₁) := C
 variables {C : Type u₁} [𝒞 : category.{v₁} C]
 include 𝒞
 
-instance core_category : groupoid.{(max v₁ 1)} (core C) :=
+instance core_category : groupoid.{v₁} (core C) :=
 { hom  := λ X Y : C, X ≅ Y,
   inv  := λ X Y f, iso.symm f,
   id   := λ X, iso.refl X,

src/category_theory/currying.lean

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

src/category_theory/discrete_category.lean

@@ -11,7 +11,6 @@ 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 {α : Type u₁} [fintype α] : fintype (discrete α) :=

src/category_theory/endomorphism.lean

@@ -14,13 +14,13 @@ universes v v' u u'
 namespace category_theory
 
 /-- Endomorphisms of an object in a category. Arguments order in multiplication agrees with `function.comp`, not with `category.comp`. -/
-def End {C : Type u} [𝒞_struct : category_struct.{v+1} C] (X : C) := X ⟶ X
+def End {C : Type u} [𝒞_struct : category_struct.{v} C] (X : C) := X ⟶ X
 
 namespace End
 
 section struct
 
-variables {C : Type u} [𝒞_struct : category_struct.{v+1} C] (X : C)
+variables {C : Type u} [𝒞_struct : category_struct.{v} C] (X : C)
 include 𝒞_struct
 
 instance has_one : has_one (End X) := ⟨𝟙 X⟩
@@ -37,27 +37,27 @@ variable {X}
 end struct
 
 /-- Endomorphisms of an object form a monoid -/
-instance monoid {C : Type u} [category.{v+1} C] {X : C} : monoid (End X) :=
+instance monoid {C : Type u} [category.{v} C] {X : C} : monoid (End X) :=
 { mul_one := category.id_comp C,
   one_mul := category.comp_id C,
   mul_assoc := λ x y z, (category.assoc C z y x).symm,
   ..End.has_mul X, ..End.has_one X }
 
 /-- In a groupoid, endomorphisms form a group -/
-instance group {C : Type u} [groupoid.{v+1} C] (X : C) : group (End X) :=
+instance group {C : Type u} [groupoid.{v} C] (X : C) : group (End X) :=
 { mul_left_inv := groupoid.comp_inv C, inv := groupoid.inv, ..End.monoid }
 
 end End
 
-def Aut {C : Type u} [𝒞 : category.{v+1} C] (X : C) := X ≅ X
+variables {C : Type u} [𝒞 : category.{v} C] (X : C)
+include 𝒞
+
+def Aut (X : C) := X ≅ X
 
 attribute [extensionality Aut] iso.ext
 
 namespace Aut
 
-variables {C : Type u} [𝒞 : category.{v+1} C] (X : C)
-include 𝒞
-
 instance: group (Aut X) :=
 by refine { one := iso.refl X,
             inv := iso.symm,
@@ -74,8 +74,8 @@ end Aut
 
 namespace functor
 
-variables {C : Type u} [𝒞 : category.{v+1} C] {D : Type u'} [𝒟 : category.{v'+1} D] (f : C ⥤ D) {X : C}
-include 𝒞 𝒟
+variables {D : Type u'} [𝒟 : category.{v'} D] (f : C ⥤ D) {X}
+include 𝒟
 
 def map_End : End X → End (f.obj X) := functor.map f
 
@@ -90,8 +90,8 @@ instance map_Aut.is_group_hom : is_group_hom (f.map_Aut : Aut X → Aut (f.obj X
 
 end functor
 
-instance functor.map_End_is_group_hom {C : Type u} [𝒞 : groupoid.{v+1} C]
-                                      {D : Type u'} [𝒟 : groupoid.{v'+1} D] (f : C ⥤ D) {X : C} :
+instance functor.map_End_is_group_hom {C : Type u} [𝒞 : groupoid.{v} C]
+                                      {D : Type u'} [𝒟 : groupoid.{v'} D] (f : C ⥤ D) {X : C} :
   is_group_hom (f.map_End : End X → End (f.obj X)) :=
 { ..functor.map_End.is_monoid_hom f }
 

src/category_theory/functor_category.lean

@@ -23,7 +23,7 @@ this is another small category at that level.
 However if `C` and `D` are both large categories at the same universe level,
 this is a small category at the next higher level.
 -/
-instance functor.category : category.{(max (u₁+1) v₂)} (C ⥤ D) :=
+instance functor.category : category.{(max u₁ v₂)} (C ⥤ D) :=
 { hom     := λ F G, nat_trans F G,
   id      := λ F, nat_trans.id F,
   comp    := λ _ _ _ α β, vcomp α β }

src/category_theory/groupoid.lean

@@ -11,7 +11,7 @@ namespace category_theory
 
 universes v u -- declare the `v`'s first; see `category_theory.category` for an explanation
 
-class groupoid (obj : Type u) extends category.{v} obj : Type (max u v) :=
+class groupoid (obj : Type u) extends category.{v} obj : Type (max u (v+1)) :=
 (inv       : Π {X Y : obj}, (X ⟶ Y) → (Y ⟶ X))
 (inv_comp' : ∀ {X Y : obj} (f : X ⟶ Y), comp (inv f) f = id Y . obviously)
 (comp_inv' : ∀ {X Y : obj} (f : X ⟶ Y), comp f (inv f) = id X . obviously)
@@ -21,8 +21,8 @@ restate_axiom groupoid.comp_inv'
 
 attribute [simp] groupoid.inv_comp groupoid.comp_inv
 
-abbreviation large_groupoid (C : Type (u+1)) : Type (u+1) := groupoid.{u+1} C
-abbreviation small_groupoid (C : Type u) : Type (u+1) := groupoid.{u+1} C
+abbreviation large_groupoid (C : Type (u+1)) : Type (u+1) := groupoid.{u} C
+abbreviation small_groupoid (C : Type u) : Type (u+1) := groupoid.{u} C
 
 instance of_groupoid {C : Type u} [groupoid.{v} C] {X Y : C} (f : X ⟶ Y) : is_iso f :=
 { inv := groupoid.inv f }

src/category_theory/hom_functor.lean

@@ -17,7 +17,7 @@ open category_theory
 
 namespace category_theory.functor
 
-variables (C : Type u) [𝒞 : category.{v+1} C]
+variables (C : Type u) [𝒞 : category.{v} C]
 include 𝒞
 
 /-- `functor.hom` is the hom-pairing, sending (X,Y) to X → Y, contravariant in X and covariant in Y. -/

src/category_theory/limits/cones.lean

@@ -18,7 +18,7 @@ open category_theory
 -- not into `Sort v`.
 -- So we don't allow this case; it's not particularly useful anyway.
 variables {J : Type v} [small_category J]
-variables {C : Type u} [𝒞 : category.{v+1} C]
+variables {C : Type u} [𝒞 : category.{v} C]
 include 𝒞
 
 open category_theory
@@ -207,7 +207,7 @@ attribute [simp] cone_morphism.w
   (w : f.hom = g.hom) : f = g :=
 by cases f; cases g; simpa using w
 
-instance cone.category : category.{v+1} (cone F) :=
+instance cone.category : category.{v} (cone F) :=
 { hom  := λ A B, cone_morphism A B,
   comp := λ X Y Z f g,
   { hom := f.hom ≫ g.hom,
@@ -266,7 +266,7 @@ def forget : cone F ⥤ C :=
 @[simp] lemma forget_map {s t : cone F} {f : s ⟶ t} : forget.map f = f.hom := rfl
 
 section
-variables {D : Type u'} [𝒟 : category.{v+1} D]
+variables {D : Type u'} [𝒟 : category.{v} D]
 include 𝒟
 
 @[simp] def functoriality (G : C ⥤ D) : cone F ⥤ cone (F ⋙ G) :=
@@ -291,7 +291,7 @@ attribute [simp] cocone_morphism.w
   {A B : cocone F} {f g : cocone_morphism A B} (w : f.hom = g.hom) : f = g :=
 by cases f; cases g; simpa using w
 
-instance cocone.category : category.{v+1} (cocone F) :=
+instance cocone.category : category.{v} (cocone F) :=
 { hom  := λ A B, cocone_morphism A B,
   comp := λ _ _ _ f g,
   { hom := f.hom ≫ g.hom,
@@ -348,7 +348,7 @@ def forget : cocone F ⥤ C :=
 @[simp] lemma forget_map {s t : cocone F} {f : s ⟶ t} : forget.map f = f.hom := rfl
 
 section
-variables {D : Type u'} [𝒟 : category.{v+1} D]
+variables {D : Type u'} [𝒟 : category.{v} D]
 include 𝒟
 
 @[simp] def functoriality (G : C ⥤ D) : cocone F ⥤ cocone (F ⋙ G) :=
@@ -365,7 +365,7 @@ end limits
 
 namespace functor
 
-variables {D : Type u'} [category.{v+1} D]
+variables {D : Type u'} [category.{v} D]
 variables {F : J ⥤ C} {G : J ⥤ C} (H : C ⥤ D)
 
 open category_theory.limits

src/category_theory/limits/functor_category.lean

@@ -12,7 +12,7 @@ namespace category_theory.limits
 
 universes v u -- declare the `v`'s first; see `category_theory.category` for an explanation
 
-variables {C : Type u} [𝒞 : category.{v+1} C]
+variables {C : Type u} [𝒞 : category.{v} C]
 include 𝒞
 
 variables {J K : Type v} [small_category J] [small_category K]