# Commit 2020-04-11 22:53 ee8cb15a

View on Github →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.