(C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.HasShift C ℤ] →
        ℤ →
          CategoryTheory.Functor (CategoryTheory.Pretriangulated.Triangle C) (CategoryTheory.Pretriangulated.Triangle C)