{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasCofilteredLimitsOfSize.{w, w', v, u} C] →
      {motive : CategoryTheory.AB5StarOfSize.{w, w', v, u} C → Sort u_1} →
        ((ofShape :
              ∀ (J : Type w') [inst_2 : CategoryTheory.Category.{w, w'} J] [inst_3 : CategoryTheory.IsCofiltered J],
                CategoryTheory.HasExactLimitsOfShape J C) →
            motive ⋯) →
          (t : CategoryTheory.AB5StarOfSize.{w, w', v, u} C) → motive t