∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z) (h : Z ⟶ (CategoryTheory.shiftFunctor C 1).obj X),
  (CategoryTheory.Pretriangulated.Triangle.mk f g h).mor₂ = g