Comma categories are locally small

We introduce instances showing that the various comma categories are locally small when the relevant categories that are involved are locally small.

instance CategoryTheory.Comma.locallySmall {A : Type u₁} {B : Type u₂} {T : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) [CategoryTheory.LocallySmall.{w, v₁, u₁} A] [CategoryTheory.LocallySmall.{w, v₂, u₂} B] : CategoryTheory.LocallySmall.{w, max v₁ v₂, max (max u₂ u₁) v₃} (CategoryTheory.Comma L R)

instance CategoryTheory.StructuredArrow.locallySmall {B : Type u₂} {T : Type u₃} [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} T] (S : T) (T✝ : CategoryTheory.Functor B T) [CategoryTheory.LocallySmall.{w, v₂, u₂} B] : CategoryTheory.LocallySmall.{w, v₂, max u₂ v₃} (CategoryTheory.StructuredArrow S T✝)

instance CategoryTheory.CostructuredArrow.locallySmall {A : Type u₁} {T : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₃, u₃} T] (S : CategoryTheory.Functor A T) (X : T) [CategoryTheory.LocallySmall.{w, v₁, u₁} A] : CategoryTheory.LocallySmall.{w, v₁, max u₁ v₃} (CategoryTheory.CostructuredArrow S X)

instance CategoryTheory.Over.locallySmall {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (X : T) [CategoryTheory.LocallySmall.{w, v₃, u₃} T] : CategoryTheory.LocallySmall.{w, v₃, max u₃ v₃} (CategoryTheory.Over X)

instance CategoryTheory.Under.locallySmall {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (X : T) [CategoryTheory.LocallySmall.{w, v₃, u₃} T] : CategoryTheory.LocallySmall.{w, v₃, max u₃ v₃} (CategoryTheory.Under X)