∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.HasShift C ℤ] {J : Type u_4}
  [inst_2 : CategoryTheory.Category.{u_3, u_4} J]
  (A B : CategoryTheory.Functor J (CategoryTheory.Pretriangulated.Triangle C))
  (hom₁ : A.comp CategoryTheory.Pretriangulated.Triangle.π₁ ⟶ B.comp CategoryTheory.Pretriangulated.Triangle.π₁)
  (hom₂ : A.comp CategoryTheory.Pretriangulated.Triangle.π₂ ⟶ B.comp CategoryTheory.Pretriangulated.Triangle.π₂)
  (hom₃ : A.comp CategoryTheory.Pretriangulated.Triangle.π₃ ⟶ B.comp CategoryTheory.Pretriangulated.Triangle.π₃)
  (comm₁ :
    CategoryTheory.CategoryStruct.comp (A.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₁Toπ₂) hom₂ =
      CategoryTheory.CategoryStruct.comp hom₁ (B.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₁Toπ₂))
  (comm₂ :
    CategoryTheory.CategoryStruct.comp (A.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₂Toπ₃) hom₃ =
      CategoryTheory.CategoryStruct.comp hom₂ (B.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₂Toπ₃))
  (comm₃ :
    CategoryTheory.CategoryStruct.comp (A.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₃Toπ₁)
        (CategoryTheory.Functor.whiskerRight hom₁ (CategoryTheory.shiftFunctor C 1)) =
      CategoryTheory.CategoryStruct.comp hom₃ (B.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₃Toπ₁))
  (x x_1 : J) (φ : x ⟶ x_1),
  CategoryTheory.CategoryStruct.comp (A.map φ)
      { hom₁ := hom₁.app x_1, hom₂ := hom₂.app x_1, hom₃ := hom₃.app x_1, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ } =
    CategoryTheory.CategoryStruct.comp
      { hom₁ := hom₁.app x, hom₂ := hom₂.app x, hom₃ := hom₃.app x, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ } (B.map φ)