Make `prod` a primitive record

Although we must work around three bugs ([bug #3481](https://coq.inria.fr/bugs/show_bug.cgi?id=3481), [bug #3507](https://coq.inria.fr/bugs/show_bug.cgi?id=3507), and [bug #3539](https://coq.inria.fr/bugs/show_bug.cgi?id=3539)), the work-arounds are relatively minor, so I'm in favor of merging this rather than waiting for @mattam82 to fix those bugs.  (For example, I want to prove the functor version of `equiv_prod_assoc`, but if we don't have eta, then it needs to assume `Funext` and do annoying transports across `path_forall`.)

This gives us a hefty speed-up in categories/Comma/ProjectionFunctors (from 22s down to 9s).  (Making everything primitive records takes a lot more bug-working-around, but brings us an overall 2x speedup, approximately.)

Note: This updates the version of Coq that we depend on, so you may have to rebuild Coq to get this code to work.
But `exact _` uses a tactic I (i.e. a newbie reading the code) already know, and a notation `_` that you I already know, so it's easy to remember and use, even if it helps to include a bit of a comment.