feat: the monoidal structure on graded objects

[kim-em]

Joint work with @joelriou.

---

[TwoFX]

Hi @semorrison, this PR is currently quite a daunting task to review. Would you mind splitting it up into smaller PRs? I'm happy to review the categorical parts of the PR, but I feel that I'm not the best person to review the changes to the three low-level files, so I would prefer if these were in a different PR (which would also be more visible to the right reviewers).

[kim-em]

Sorry, I don't anticipate having much time to doing substantial new work here, e.g. splitting up the PR. Hopefully someone might want to adopt it, or at least it can be inspiration that this is possible when someone needs it.

[joelriou]

I think I will adopt this PR, and refactor it so as to allow further useful generalizations. The idea would be to "extend" a bifunctor F : C₁ ⥤ C₂ ⥤ C₃ to a functor GradedObject I C₁ ⥤ GradedObject J C₂ ⥤ GradedObject (I × J) C₃ and to introduce a kind of "integration" for GradedObject. This would be a functor GradedObject.map C φ : GradedObject I C ⥤ GradedObject I' C attached to a map φ : I → I' which would use some coproducts in C. In case I is a monoid and φ is the addition, we shall get a functor GradedObject (I × I) C₃ ⥤ GradedObject I C₃, and using this, we could "extend" F to a functor GradedObject I C₁ ⥤ GradedObject I C₂ ⥤ GradedObject I C₃.

In case the functor F is the tensor product for a monoidal category C, this will give a candidate tensor functor for a monoidal category structure on GradedObject I C. Then, developing a suitable API for these constructions, we should recover the main result of this PR in the case I := ℕ, but I think it is important to develop slightly more general results (both in terms of the index set I and the bifunctor), because at some point, I would like to consider tensor products of unbounded complexes...

[kim-em]

@joelriou, great to hear, I look forward to seeing what you come up with. Please feel free to close this PR either immediately or later.