∀ (C : Type u_2) [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ} (φ : T₁ ⟶ T₂),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Pretriangulated.Triangle.mk T₂.mor₂.unop T₂.mor₁.unop
          (CategoryTheory.CategoryStruct.comp
            ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C 1).unitIso.inv.app T₂.obj₁).unop
            ((CategoryTheory.shiftFunctor C 1).map T₂.mor₃.unop))).mor₂
      φ.hom₁.unop =
    CategoryTheory.CategoryStruct.comp φ.hom₂.unop
      (CategoryTheory.Pretriangulated.Triangle.mk T₁.mor₂.unop T₁.mor₁.unop
          (CategoryTheory.CategoryStruct.comp
            ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C 1).unitIso.inv.app T₁.obj₁).unop
            ((CategoryTheory.shiftFunctor C 1).map T₁.mor₃.unop))).mor₂