Reduce universes in Spaces.No

[jdchristensen]

While looking at Spaces.No.Core recentlly, I realized that the lines

  Context {S : OptionSort@{i}}.

and

  Private Inductive Game : Type := | opt : forall (L R : Type@{i}) ...

were inadvertently introducing independent universe variables denoted i, when the intention was that they be the same variable. As a result, Game had two universe variables, which were constrained to be equal. The fix is simply to add Universe i. before the first line above, to declare i as a universe variable throughout the section. This is the content of the first commit, which therefore must also change Game@{i} to Game throughout (since Game@{i} is actually referring to two universe variables, since one is in the context). This reduces by one the number of universe variables in most subsequent results as well.

The second commit is purely cosmetic, replacing InSort@{i} with InSort, since there is no ambiguity at all now.

The third commit moves the inductive type No_Empty_for_admitted earlier in the section. For some reason, it depended on six universe variables. Moving it earlier gets rid of five, and putting it in Type0 gets rid of the last one. This has a big impact. For example, plus in Spaces.No.Addtion goes from 157 variables to 88. And the build times slightly improve.

Changes similar to those in the first two commits will need to be done in github1759.v in #1773 . I'm happy to rebase that commit and push the fix there once this is merged. (Or if that is merged first, I'll rebase this and push the fix.)

[Alizter]

Seems OK to me. I don't mind merging this one before since the other one might need some time to be looked at.

[jdchristensen]

@Alizter Do you want me to rebase #1773?

[Alizter]

@jdchristensen That would be great!