∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {A : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  {B : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃}
  [inst_3 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T}
  [CategoryTheory.Limits.HasColimitsOfShape J A] [CategoryTheory.Limits.HasColimitsOfShape J B]
  [CategoryTheory.Limits.PreservesColimitsOfShape J L],
  CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.Comma.fst L R)