fix(algebra/category/Module/colimits): generalize universes (#11802)

src/algebra/category/Module/colimits.lean

@@ -20,12 +20,12 @@ In fact, in `Module R` there is a much nicer model of colimits as quotients
 of finitely supported functions, and we really should implement this as well (or instead).
 -/
 
-universes u v
+universes u v w
 
 open category_theory
 open category_theory.limits
 
-variables {R : Type v} [ring R]
+variables {R : Type u} [ring R]
 
 -- [ROBOT VOICE]:
 -- You should pretend for now that this file was automatically generated.
@@ -39,7 +39,7 @@ then taking the quotient by the abelian group laws within each abelian group,
 and the identifications given by the morphisms in the diagram.
 -/
 
-variables {J : Type v} [small_category J] (F : J ⥤ Module.{v} R)
+variables {J : Type w} [category.{v} J] (F : J ⥤ Module.{max u v w} R)
 
 /--
 An inductive type representing all module expressions (without relations)
@@ -104,7 +104,7 @@ attribute [instance] colimit_setoid
 The underlying type of the colimit of a diagram in `Module R`.
 -/
 @[derive inhabited]
-def colimit_type : Type v := quotient (colimit_setoid F)
+def colimit_type : Type (max u v w) := quotient (colimit_setoid F)
 
 instance : add_comm_group (colimit_type F) :=
 { zero :=
@@ -268,7 +268,7 @@ begin
   apply relation.map,
 end
 
-@[simp] lemma cocone_naturality_components (j j' : J) (f : j ⟶ j') (x : F.obj j):
+@[simp] lemma cocone_naturality_components (j j' : J) (f : j ⟶ j') (x : F.obj j) :
   (cocone_morphism F j') (F.map f x) = (cocone_morphism F j) x :=
 by { rw ←cocone_naturality F f, refl }
 
@@ -365,7 +365,7 @@ def colimit_cocone_is_colimit : is_colimit (colimit_cocone F) :=
     refl
   end }.
 
-instance has_colimits_Module : has_colimits (Module R) :=
+instance has_colimits_Module : has_colimits (Module.{max v u} R) :=
 { has_colimits_of_shape := λ J 𝒥, by exactI
   { has_colimit := λ F, has_colimit.mk
     { cocone := colimit_cocone F,