Zulip Chat Archive

Stream: new members

Topic: Universe Polymorphic natural numbers


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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