Triangle-closure conditions on opposite subcategories

Third-object closure of an object property in a pretriangulated category gives first-object closure of the opposite property. This instance allows arguments using first-object closure to be applied to the opposite category.

instance CategoryTheory.ObjectProperty.instIsTriangulatedClosed₁OppositeOpOfIsTriangulatedClosed₃_tauCeti {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsTriangulatedClosed₃] : P.op.IsTriangulatedClosed₁

Third-object closure of a property becomes first-object closure on the opposite category.