Comma categories project to product categories

Construct the projection functor.  Ported from CommaCategoryProjection.v
at
https://bitbucket.org/JasonGross/catdb/src/4eb6407c6ca3200bebefaa3a1834d05c49b01846/CommaCategoryProjection.v?at=default.
I don't have the energy right now to port CommaCategoryInducedFunctors.v
at
https://bitbucket.org/JasonGross/catdb/src/4eb6407c6ca3200bebefaa3a1834d05c49b01846/CommaCategoryInducedFunctors.v?at=default
or the more complicated CommaCategoryProjectionFunctors.v.