{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      [inst_2 : CategoryTheory.Preadditive C] →
        [inst_3 : CategoryTheory.Limits.HasZeroObject C] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              {W : CategoryTheory.MorphismProperty C} →
                {motive : W.IsCompatibleWithTriangulation → Sort u} →
                  ([toIsCompatibleWithShift : W.IsCompatibleWithShift ℤ] →
                      (compatible_with_triangulation :
                          ∀ (T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C),
                            T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
                              T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
                                ∀ (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂),
                                  W a →
                                    W b →
                                      CategoryTheory.CategoryStruct.comp T₁.mor₁ b =
                                          CategoryTheory.CategoryStruct.comp a T₂.mor₁ →
                                        ∃ c,
                                          ∃ (_ : W c),
                                            CategoryTheory.CategoryStruct.comp T₁.mor₂ c =
                                                CategoryTheory.CategoryStruct.comp b T₂.mor₂ ∧
                                              CategoryTheory.CategoryStruct.comp T₁.mor₃
                                                  ((CategoryTheory.shiftFunctor C 1).map a) =
                                                CategoryTheory.CategoryStruct.comp c T₂.mor₃) →
                        motive ⋯) →
                    (t : W.IsCompatibleWithTriangulation) → motive t