Coq-HoTT
Coq-HoTT copied to clipboard
HoTT
Use explicit universe constraints
Apparently our hacks like
Definition Type2@{i j} := Eval hnf in let gt := (Type1@{j} : Type@{i}) in Type@{i}.
can now be replaced with
Definition Type2@{i j | Set < j, j < i} := Type@{i}.
I'm not following Coq versions and releases; I just had this possibility pointed to me on CT Zulip and checked for myself that it works.
Nice! I just checked, it works with 8.13 so we just need to do it at some point.
Nice! It's documented at https://coq.inria.fr/refman/addendum/universe-polymorphism.html (search for univ_constraint).
This feature is even more useful than I expected: if you declare some constraints, then Coq won't silently add additional constraints beyond those implied by the specification. (This doesn't seem to be documented, but is great.) This makes things much, much more robust. It also eliminates the need to add comments saying what the universe constraints are (comments that could be wrong since they aren't checked and can be affected by changes elsewhere in the library).
A few more details. If you intend for there to be no constraints between universe variables, you can use @{i j k | } to enforce this. If you want to impose some constraints and allow Coq to generate additional constraints, then @{i j k | i <= j +} seems to indicate this. (Again, not documented as far as I can see.)
I think that just about anywhere where we bother to list the universe variables in a definition, we should probably list the constraints.
BTW, I noticed that we use none of Type1, Type2, Type3, Type2le, Type3le in the library. Since their effects can be easily achieved with universe contraints now, I think we should delete them all from Overture.v. I can do this unless I hear an argument against it.
We also don't need Basics/UniverseLevel.v anymore. It is used in one place in Metatheory/FunextVarieties.v, but that one place can be simplified a lot using universe constraint annotations. Should I get rid of UniverseLevel.v? Or move it to the Metatheory folder?
I'm now thinking of creating a folder theories/Misc that could contain UniverseLevel.v and many of the top-level .v files that don't have a natural home. I would also remove the Misc.v file that is currently empty.