HoTT/HoTT — pull request #472 by JasonGross (2014-09-08 09:18:56+00:00)
Title: Make PreCategory a primitive record

This gives us a substantial speedup (15% overall), and reduces the kinds of opposite functors and opposite natural transformations we need.

The only bug to be worked around here is that tactics do not work up to record eta. @mattam82 is aware of this, and I think he is considering having `rewrite`, `apply`, etc work up to user-defined classes of head constants, as is done in Matita, and which Enrico suggested on coqdev. However, I suspect this issue will not be resolved anytime soon, so I don't want to wait for that to merge this.

Next up: Functors. Then natural transformations. Then pseudofunctors and adjoints. Then the rest of categories, possibly barring the typeclasses. Then the rest of the core library, again possibly barring typeclasses, where I seem to recall there being more issues than in other places.