copumpkin/categories — pull request #4 by JasonGross (2013-06-06 04:21:17+00:00)
Title: 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.