∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) {A : Type u_2}
  {B : Type u_3} {J : Type u_4} [inst_1 : CategoryTheory.Category.{v_2, u_2} A]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} B] [inst_3 : CategoryTheory.Category.{v_4, u_4} J]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T}
  [CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.Comma L R)]
  [(CategoryTheory.MorphismProperty.commaObj L R P).IsClosedUnderColimitsOfShape J],
  CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.MorphismProperty.Comma L R P ⊤ ⊤)