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.