Pretriangulated category

In the convention used by mathlib, a pretriangulated category is a preadditive category with a zero object, an additive shift $[1]$ (so $(f+g)[1]=f[1]+g[1]$ and $0[1]=0$), and a class Δ of triangles, whose members are called distinguished, satisfying:

1. distinguishedness is preserved by isomorphism;
2. every contractible triangle $X\xrightarrow{\mathrm{id}_X}X\to0\to X[1]$ is distinguished;
3. every morphism extends to a distinguished triangle;
4. $X\xrightarrow fY\xrightarrow gZ\xrightarrow hX[1]$ is distinguished exactly when its rotation $Y\xrightarrow gZ\xrightarrow hX[1]\xrightarrow{-f[1]}Y[1]$ is;
5. a commuting square on the first maps of two distinguished triangles extends to a morphism of triangles.