TODO remove floating universe in peano_naturals

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory

http://homotopytypetheory.org/

Other

1.25k stars 193 forks source link

TODO remove floating universe in peano_naturals #1722

Open SkySkimmer opened 1 year ago

SkySkimmer commented 1 year ago

peano_naturals.v says

(* This should go away one Coq has universe cumulativity through inductives. *)
Section nat_lift.

Universe N.

Let natpaths := @paths@{N} nat.
Infix "=N=" := natpaths.

then writes everything @{N}.

Now that cumulativity exists it may be time to remove the N universe.

NB: attempts will probably hit https://github.com/HoTT/Coq-HoTT/pull/1721#issuecomment-1445035678 since goals will become @paths@{Set} nat _ _ and nat_rec is defined as Minimality (in Spaces.Nat.Core)

jdchristensen commented 1 year ago

Actually, this file builds fine with all universe annotations removed and various minor changes. But then Classes/theory/naturals.v fails to build, as it can't find lots of instances. For example, ?Azero0 : "Zero nat". This is similar to what I found in #1721 where Coq couldn't find instances for IsHProp Unit after some things were minimized to set. Do you want me to PR the changes to peano_naturals.v so you can experiment further?

SkySkimmer commented 1 year ago

I don't really have the time

jdchristensen commented 1 year ago

I made the PR anyways, just to record the changes in case someone wants to continue work on it.