HoTT/HoTT — pull request #387 by JasonGross (2014-05-08 21:12:22+00:00)
Title: 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.