The UniMath library has a formalization on abelian categories and homological algebra (done by Tommi Pannila). See:

• https://github.com/UniMath/UniMath/blob/master/UniMath/CategoryTheory/Abelian.v
• https://github.com/UniMath/UniMath/blob/master/UniMath/CategoryTheory/ShortExactSequences.v
• https://github.com/UniMath/UniMath/blob/master/UniMath/CategoryTheory/FiveLemma.v

The documentation can be found here: https://github.com/tpannila/Masters_thesis/blob/master/An%20Introduction%20to%20Homological%20Algebra.pdf

The UniMath library has a formalization on abelian categories and homological algebra (done by Tommi Pannila). See:

• Abelian categories
• Short exact sequences
• Five lemma

The documentation can be found here: An Introduction to Homological Algebra