mathlib3

6b182fcd - feat(category_theory/triangulated/pretriangulated): add definition of pretriangulated categories and triangulated functors between them (#7153)

feat(category_theory/triangulated/pretriangulated): add definition of pretriangulated categories and triangulated functors between them (#7153) Adds a definition of pretriangulated categories and triangulated functors between them. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>