{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {motive : CategoryTheory.Limits.HasCofilteredLimitsOfSize.{w', w, v, u} C → Sort u_1} →
      (t : CategoryTheory.Limits.HasCofilteredLimitsOfSize.{w', w, v, u} C) →
        ((HasLimitsOfShape :
              ∀ (I : Type w) [inst_1 : CategoryTheory.Category.{w', w} I] [CategoryTheory.IsCofiltered I],
                CategoryTheory.Limits.HasLimitsOfShape I C) →
            motive ⋯) →
          motive t