feat: the homological functor on the homotopy category of cochain complexes in an abelian category

[joelriou]

trafficstars

The homology functors on the homotopy category of cochain complexes in an abelian category are homological functors (in the sense that they send distinguished triangles to exact sequences). This PR also shows that the category of homological complexes in an abelian category is an abelian category.

---

This is a draft.

• [ ] depends on: #11740
• [ ] depends on: #11759