feat(category/functor): make sum functor instance more universe p…

…olymorphic

category/functor.lean

@@ -109,16 +109,16 @@ end ulift
 
 namespace sum
 
-variables {γ α β : Type v}
+variables {γ : Type u} {α β : Type v}
 
 protected def mapr (f : α → β) : γ ⊕ α → γ ⊕ β
 | (inl x) := inl x
 | (inr x) := inr (f x)
 
-instance : functor (sum γ) :=
+instance : functor (sum.{u v} γ) :=
 { map := @sum.mapr γ }
 
-instance : is_lawful_functor.{v} (sum γ) :=
+instance : is_lawful_functor (sum γ) :=
 { id_map := by intros; casesm _ ⊕ _; refl,
   comp_map := by intros; casesm _ ⊕ _; refl }