∀ {T : Type u_6} [inst : CategoryTheory.Category.{u_5, u_6} T] (P : CategoryTheory.MorphismProperty T) {A : Type u_2}
  {B : Type u_4} {J : Type u_8} [inst_1 : CategoryTheory.Category.{u_1, u_2} A]
  [inst_2 : CategoryTheory.Category.{u_3, u_4} B] [inst_3 : CategoryTheory.Category.{u_7, u_8} J]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T}
  (D : CategoryTheory.Functor J (CategoryTheory.MorphismProperty.Comma L R P ⊤ ⊤))
  [(CategoryTheory.MorphismProperty.commaObj L R P).IsClosedUnderLimitsOfShape J]
  [inst_5 : CategoryTheory.Limits.HasLimit (D.comp (CategoryTheory.MorphismProperty.Comma.forget L R P ⊤ ⊤))],
  CategoryTheory.MorphismProperty.commaObj L R P
    (CategoryTheory.Limits.limit (D.comp (CategoryTheory.MorphismProperty.Comma.forget L R P ⊤ ⊤)))