feat(category_theory/monoidal): the definition of Tor (#7512)

Tor, the left-derived functor of tensor product

We define tor C n : C ⥤ C ⥤ C, by left-deriving in the second factor of (X, Y) ↦ X ⊗ Y. For now we have almost nothing to say about it! It would be good to show that this is naturally isomorphic to the functor obtained by left-deriving in the first factor, instead.