A * (B * C) ≅ (A * B) * C, for categories

This is on top of #429.
Responding to @spitters comment on the commit (here, so it sticks around even if I rebase)

> These names are very generic, but I guess that is OK, since they are in the Module.

Yes, the idea is that they will be used as `Associativity.functor` or `ProductLaws.Associatvity.functor`, and that you'll never import this module.