feat(algebra/category/Module): arbitrary colimits (#7099)
This is just the "semi-automated" construction of arbitrary colimits in the category or `R`-modules, following the same model as for `Mon`, `AddCommGroup`, etc.
We already have finite colimits from the `abelian` instance. One could also give definitionally nicer colimits as quotients of finitely supported functions. But this is better than nothing!
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
