∀ {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 : ⦃X Y : C⦄ → (x : X ⟶ Y) → W.colimitsOfShape J x → Prop},
  (∀ (X₁ X₂ : CategoryTheory.Functor J C) (c₁ : CategoryTheory.Limits.Cocone X₁) (c₂ : CategoryTheory.Limits.Cocone X₂)
      (h₁ : CategoryTheory.Limits.IsColimit c₁) (h₂ : CategoryTheory.Limits.IsColimit c₂) (f : X₁ ⟶ X₂)
      (x : W.functorCategory J f), motive (h₁.desc { pt := c₂.pt, ι := CategoryTheory.CategoryStruct.comp f c₂.ι }) ⋯) →
    ∀ ⦃X Y : C⦄ {x : X ⟶ Y} (t : W.colimitsOfShape J x), motive x t