## Stream: new members

### Topic: Universe Polymorphic natural numbers

#### Luiz Carlos Rumbelsperger Viana (May 14 2020 at 14:54):

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 (May 14 2020 at 14:56):

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 (May 14 2020 at 15:00):

@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.

Last updated: May 14 2021 at 23:14 UTC