Pre polyproj fixups

In working on getting HoTT working with the polyproj branch (#301), Matthieu and I made a bunch of changes.  In order to see clearly which changes point to bugs in coq, I'm going to merge the improvements that compile with HoTT/coq, and are for well-understood reasons (handling of opacity has changed) or are cosmetic.  Since this mostly only touches the category code, and not in any deep way, I'll merge it as soon as I check that it builds correctly.