∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (T : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ),
  T ∈ CategoryTheory.Pretriangulated.Opposite.distinguishedTriangles C ↔
    ∃ T',
      ∃ (_ : T' ∈ CategoryTheory.Pretriangulated.distinguishedTriangles),
        Nonempty (T ≅ (CategoryTheory.Pretriangulated.triangleOpEquivalence C).functor.obj (Opposite.op T'))