feat(category_theory): functorial images (#2373)
This is the first in a series of most likely three PRs about the cohomology functor. In this PR, I
* add documentation for `comma.lean`,
* introduce the arrow category as a special case of the comma construction, and
* introduce the notion of functorial images, which means that commutative squares induce morphisms on images making the obvious diagram commute.
