Split out InitialTerminalCategory.v into multiple files

This way, we can add pseudofunctors without making the
initial/terminal categories depend on them.
Add pseudofunctors from initial/terminal categories

These will be useful for lax slice categories
Add an instance about [idtoiso] and [components_of]
Define the identity pseudofunctor
WIP
WIP move to pseudofunctors
More WIP

Next step is to give versions of the lemmas for rewrite for the
inverses, and then do the same munging we did in the Grothendieck
construction here, for speed, to prove the identity laws.
Make inverse rewrite laws for pseudofunctor
Add [unique pose proof] and [unique pose] to Tactics.v
Add some typeclass resolution hints for apply being stupid

[apply] doesn't know that, e.g., the identity functor applied to x is
x, nor vice-versa.  And because it infers arguments in the "wrong"
order, it errors before it has a chance to pick up that information.
So we need to help it along a little.
Add some convenience lemmas for removing isomorphisms
Mostly finish lax comma categories
Fix core
Remove useless includes