TODO remove floating universe in peano_naturals

[SkySkimmer]

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 #1721 (comment) since goals will become @paths@{Set} nat _ _ and nat_rec is defined as Minimality (in Spaces.Nat.Core)

[jdchristensen]

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]

I don't really have the time

[jdchristensen]

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