feat(category_theory/commas): add simp-lemmas for comma categories

[jcommelin]

Add comma categories and basic functoriality properties

TO CONTRIBUTORS:

Make sure you have:

• reviewed and applied the coding style: coding, naming
• make sure definitions and lemmas are put in the right files
• make sure definitions and lemmas are not redundant

For reviewers: code review check list

[rwbarton]

Much of this was already added in the limits-1 PR, though I renamed the module name to category_theory.comma because I find random pluralizations hard to remember.

[semorrison]

I'm not sure I like the section names section simp and section map_left_and_right. At least, it's not the style used elsewhere in mathlib.

Perhaps remove these, or just change them to comments, e.g. section -- simp lemmas.

Perhaps @digama0 can give a style ruling, and we can update the style guide. :-)

[semorrison]

Other than that, looks good to me.

[jcommelin]

Removed the section names.

[rwbarton]

LGTM... though it really shows how we need a better way to deal with this proliferation of simp lemmas.