Pretriangulated category

In the convention used by mathlib, a pretriangulated category is a preadditive category with a zero object, an additive shift, and a class of distinguished triangles satisfying the first triangle axioms:

1. distinguishedness is preserved by isomorphism;
2. every morphism extends to a distinguished triangle;
3. a triangle is distinguished exactly when its rotation is;
4. a commuting square on the first maps of two distinguished triangles extends to a morphism of triangles.

This terminology is convention-sensitive. Here “triangulated” means pretriangulated plus the octahedral axiom.