Primitive projections should be on by default

Version

8.8+alpha

Description of the problem

I would like to see primitive projections + eta on by default in the standard library, especially for types like and, prod, sig, sigT, sigT2, sig2, etc. Not only should this make things faster, there are also a number of useful things to be gained by having judgmental eta. (See, for example, this stack overflow comment and associated discussion.)

I think there will be two stages to this: the first is to turn the standard library constructions from Inductive into Record; this will break anyone relying on autogenerated names from destructing such pairs, but I think this is a cost worth paying, and one that is not unreasonable, given that we are tracking so many contributions in the CI.

The second stage will be to turn on primitive projections and eta. This will break developments relying on a particular unfolding order of canonical structures for these types. I think this may require more discussion. I think the most compatibility preserving option here is to add a way to disable judgmental eta in unification problems (but not conversion problems) for particular inductives, or a way to delay using eta for those records during unification. (cc @mattam82 @ggonthier @beta-ziliani )

Start by locating the standard-library definitions for and, prod, sig, sigT, sigT2, and sig2, then review how they are currently declared. The issue describes converting these constructions to records and later enabling primitive projections and eta; done requires resolving the stated compatibility concerns and implementing both stages.