Make inverse rewrite laws for pseudofunctor

These are slow, but useful for lax comma categories.

Also, split out the rewrite laws into a separate file.