feat(CategoryTheory): triangulated functors are additive

[joelriou]

---

[github-actions[bot]]

PR summary 39a554bbf1

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ instance (priority := 100) : F.Additive := F.additive_of_preserves_binary_products + instance : PreservesLimitsOfShape (Discrete WalkingPair) F := by

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style