Add an identity remover

It's currently rather slow, and reification is a pain
Merged jgross' CategorySolver
Add some more adjunction laws
Reorganize adjunctions

Prove some more laws about them, split them out into multiple files, and
use whiskering to reduce the size of the composition proofs.
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.
tightened up Categories.Comma.Functors
made more morphism manipulation mechanisms
(cherry picked from commit 041aa1666d06d79d2b68a23e0ef510c8e7290bc6)
backported AUReasoning
backported Pushes in Categories.Square
ported Categories.Comma.Functores.InducedFunctor from jgross's coq library
fixing Adjunction imports: "hiding" is not very future-proof
DinaturalTransformation: _∘>_ via duality
ported Categories.End to AUReasoning
Categories.Functor.Discrete