{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} →
                      (D : CategoryTheory.Functor J (CategoryTheory.MorphismProperty.Comma L R P ⊤ ⊤)) →
                        [(CategoryTheory.MorphismProperty.commaObj L R P).IsClosedUnderColimitsOfShape J] →
                          [CategoryTheory.Limits.HasColimit
                                (D.comp (CategoryTheory.MorphismProperty.Comma.forget L R P ⊤ ⊤))] →
                            CategoryTheory.CreatesColimit D (CategoryTheory.MorphismProperty.Comma.forget L R P ⊤ ⊤)