Zulip Chat Archive

Stream: lean4

Topic: Universes


view this post on Zulip Calvin Lee (Jan 28 2021 at 18:22):

Can I use a type with two different universes in the same declaration?
e.g. if I have def foo {m : Type u -> Type v} can I use m with two different universes in the same formula?

view this post on Zulip Kyle Miller (Jan 28 2021 at 18:32):

If they're different m's, then yes. You can even be explicit with universes if needed. Here's setting u=0 and v=1: foo.{0, 1}. This notation works with universe variables, too.

view this post on Zulip Floris van Doorn (Jan 28 2021 at 18:37):

In the definition of foo you cannot use m with a different universe level: you only have one m that has type Type u -> Type v, and u and v are fixed in the definition of foo.
After you have declared foo you can use it with u and v instantiated however you want.

view this post on Zulip Calvin Lee (Jan 28 2021 at 18:42):

Is there any way to make a tuple of items in two different universes? e.g. could I have def foo {m : Type u -> Type v} {a : Type u} ... : Option (m a, a) because I'm trying to do something like this and getting some type errors

view this post on Zulip Kyle Miller (Jan 28 2021 at 18:45):

(deleted)

view this post on Zulip Mario Carneiro (Jan 28 2021 at 18:45):

I think you want Option (m a × a)

view this post on Zulip Mario Carneiro (Jan 28 2021 at 18:46):

and this should work even if m a and a are in different universes

view this post on Zulip Floris van Doorn (Jan 28 2021 at 18:46):

If you have a pair, you can just take a product.
If you need a sequence with n elements, this gets inconvenient, but it is possible with Ulift.


Last updated: May 07 2021 at 13:21 UTC