Develop theory of additive/abelian categories

[barrettj12]

In #672, I defined (pre)additive and (pre)abelian categories. I've essentially only defined enough to formalise the construction in arxiv:2103.08379 (see #674), so there is a lot of important theory still to be formalised. I'd particularly like to see:

• [ ] Additive and exact functors
• [ ] Exact sequences
• [ ] Proofs of the snake lemma, five lemma, nine lemma, etc
• [ ] An example of an abelian category, e.g. the category of abelian groups. My work in Algebra.AbGroup.Instances.Hom was a start on this.
• [ ] In Categories.Additive.Properties, I defined matrix notation for morphisms (x₁ ⊕ ⋯ ⊕ x­­ₙ) → (y₁ ⊕ ⋯ ⊕ yₘ) in an additive category. I'd like to see some decent tools to work with this matrix algebra, for example, a lemma which can multiply an m×n matrix with an n×k matrix.
• [ ] Other fundamental results, as found in e.g. Mac Lane.

[mzhang28]

I have started some work on the definition of exact sequences and the proof of the five lemma. Has there been any progress on this issue? Hope I'm not stepping over someone else's work

[felixwellen]

This is the last thing Jordan worked on: https://github.com/agda/cubical/pull/674 Unfortunately, I didn't get to finish this draft PR, after Jordan stopped (he has stopped years ago - you are definitely not stepping on someones toes). Maybe you can make use of the draft PR?