Try to make entire library Cumulative

[jdchristensen]

This is WIP to show what fails when you try to make the entire library Cumulative. I didn't put much effort into this.

Algebra/Universal/Homomorphism.v: homomorphism_id fails, and I didn't immediately see a quick fix. So I marked one thing in that file as NonCumulative.

Modalities/Descent.v: I added a comment near the failing part here, and again wasn't sure how to fix it.

Classes/theory/premetric.v: I didn't investigate.

Sets/Hartogs.v: I didn't investigate.

Categories/Comma/ProjectionFunctors.v: spins.

There may be more failures when dependencies of those files are built, but the good news is that 406 files (out of 578) built fine, so I would guess that there will be around 2 or 3 other files with issues.

[jdchristensen]

Please feel free to experiment and to push changes if you find solutions. I'm not very familiar with most of the files with errors.

[jdchristensen]

I rebased the first two commits, and added a third which gets Modalities/* and TruncType.v building. There are currently four build failures and around 200 files not attempted. I think it would just be a matter of adding or removing some universe annotations, but I recommend waiting until Coq supports + and max in universe variables, as that will greatly reduce the number of universe variables, making the job easier.

[Alizter]

The upstream Coq PR is:

• Algebraic universes and new solving algorithm coq/coq#18903