{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {J : Type u_1} →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} J] →
          {motive : W.IsStableUnderLimitsOfShape J → Sort u_2} →
            (t : W.IsStableUnderLimitsOfShape J) →
              ((condition :
                    ∀ (X₁ X₂ : CategoryTheory.Functor J C) (c₁ : CategoryTheory.Limits.Cone X₁)
                      (c₂ : CategoryTheory.Limits.Cone X₂) (x : CategoryTheory.Limits.IsLimit c₁)
                      (h₂ : CategoryTheory.Limits.IsLimit c₂) (f : X₁ ⟶ X₂),
                      W.functorCategory J f →
                        ∀ (φ : c₁.pt ⟶ c₂.pt),
                          (∀ (j : J),
                              CategoryTheory.CategoryStruct.comp φ (c₂.π.app j) =
                                CategoryTheory.CategoryStruct.comp (c₁.π.app j) (f.app j)) →
                            W φ) →
                  motive ⋯) →
                motive t