This PR starts the construction of the cochain complex of morphisms from a cochain complex to another.

(I am sorry this PR is a little bit longer than the norm, but I wanted to include the composition of cochains.)

If F and G are two cochain complexes (indexed by the integers), I roughly define an element in Cochain F G n to be the datum of morphisms F.X p ⟶ G.X q for all integers p and q such that p + n = q. (Before I chose this design, I also experimented with a simpler definition : F.X p ⟶ G.X (p+n) for all p, but this lead to a nightmare of eqToHom popping everywhere.)

These cochains shall play a critical role in the study of the mapping cone of a morphism of cochain complexes, and in the verification of the axioms of triangulated categories for the homotopy category, which is the reason why this PR creates the file Algebra.Homology.HomotopyCategory.HomComplex.

(Note: the composition of cochains would be an example of an instance of the type class of graded heterogeneous multiplications which I attempted to introduce in #6678. I wish that the current API for graded types could be generalized in order to involve three graded types (i.e. some HMul rather than just Mul and SMul), and that the data would involve a multiplication X a → Y b → Z c whenever a + b = c rather than just X a → Y b → Z (a + b)., see the discussion there #6678. However, there is no hurry about a design decision here, because I shall not need more graded heterogeneous multiplications until the construction of the derived category of an abelian category and its triangulated structure is over...)