Universe Polymorphic natural numbers

Stream: new members

[Luiz Carlos Rumbelsperger Viana]

Is there an universe polymorphic version of the natural numbers?

Suppose I have some structure:

strucure my_struct (t : Type u) :=
(my_field : Type u := nat)
(some_other_field : t)

Here if I don't have a polymorphic version of nat, I lose universe polymorphism for my_field, since that is got to be set to Type 1. Is there any way to get universe polymorphism and still set nat as the default value?

[Reid Barton]

You can use ulift nat, but it might not have all the structure you want automatically, and pattern matching will work slightly differently, etc.

[Luiz Carlos Rumbelsperger Viana]

@Reid Barton Thanks, ulift was precisely the kind of functionality I was searching for. Didn't know where I could find it, because I didn't know its name. Now I've found it.