HoTT/HoTT — pull request #505 by JasonGross (2014-09-15 23:20:36+00:00)
Title: Make the rest of categories, bar [IsIsomorphism], primitive records

Hopefully @mattam82 will fix [bug 3624](https://coq.inria.fr/bugs/show_bug.cgi?id=3624), involving notations and named arguments, and then all of categories can be primitive records. But I don't think we have to wait for that, nor [bug 3626](https://coq.inria.fr/bugs/show_bug.cgi?id=3626), to merge this.

We're down to 2m 28s on my machine, now. Speaking of timing, @mattam82, any idea what Coq is doing when it takes 1.2s to typecheck `(idpath, idpath)` in `theories/categories/Comma/Dual.v` on this branch (definition `dual_functor_involutive`)? Have I not used primitive projections well?

Anyway, next up: the rest of the library.