Octahedral axiom

The octahedral axiom concerns composable morphisms $X\xrightarrow{f}Y\xrightarrow{g}Z$ in a pretriangulated category. Choose distinguished triangles for $f$, $g$, and $g\circ f$. The axiom requires connecting morphisms between their third objects so that the resulting octahedral diagram commutes and those third objects themselves form a distinguished triangle.

Conceptually, it states that forming cones is coherent with composition. It is often labeled TR4. In mathlib, IsTriangulated is precisely the assertion that the required octahedron exists for every such composable pair and choices of distinguished triangles.