∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) {A : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A] {L : CategoryTheory.Functor A T} [L.Faithful] [L.Full] {Y : A}
  [P.ContainsIdentities] [P.RespectsIso],
  (CategoryTheory.MorphismProperty.costructuredArrowObj L P).IsClosedUnderLimitsOfShape
    (CategoryTheory.Discrete PEmpty.{1})