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₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) [LocallySmall.{w, v₁, u₁} A] [LocallySmall.{w, v₂, u₂} B] : LocallySmall.{w, max v₁ v₂, max (max u₂ u₁) v₃} (Comma L R)

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

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

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

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