{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} →
                  (t : W.IsCompatibleWithTriangulation) →
                    ([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 ⋯) →
                      motive t