Zulip Chat Archive

Stream: general

Topic: universe polymorphic version of empty?


view this post on Zulip Zesen Qian (Jul 05 2018 at 19:13):

RT? The current empty is at Type 0

view this post on Zulip Zesen Qian (Jul 05 2018 at 19:13):

just don't want to reinvent the wheel.
Also wondering why empty is not universe polymorphic

view this post on Zulip Chris Hughes (Jul 05 2018 at 19:16):

What situation would it be an advantage for empty to be polymorphic?

view this post on Zulip Zesen Qian (Jul 05 2018 at 19:17):

oh wait, is lean's universe cumulative?

view this post on Zulip Simon Hudon (Jul 05 2018 at 19:17):

If you need empty in universe u, you can use ulift.up.{u} empty. ulift is a tool to fit objects of different universes together.

view this post on Zulip Simon Hudon (Jul 05 2018 at 19:17):

No, it's not

view this post on Zulip Zesen Qian (Jul 05 2018 at 19:17):

very nice, thank you.

view this post on Zulip Simon Hudon (Jul 05 2018 at 19:18):

we use ulift when we would need cumulativeness

view this post on Zulip Simon Hudon (Jul 05 2018 at 19:20):

In general, you should use universe variables as rarely as possible and use ulift. When you build definitions like list, you have no choice to make it universe polymorphic so that it can be used in various universes: list : Type u -> Type u. That's because if list : Type -> Type, there's no way of using lift on a : Type 3 in order to have a list a

view this post on Zulip Zesen Qian (Jul 05 2018 at 19:31):

ahh, can't understand the error
ulift Type
not match
Type u

view this post on Zulip Simon Hudon (Jul 05 2018 at 19:32):

Can you show the code?

view this post on Zulip Zesen Qian (Jul 05 2018 at 19:32):

def clause : list (Type u) → Type u
| ([]) := ulift.up.{u+1} empty
| (x :: xs) := sum x $ clause xs

view this post on Zulip Simon Hudon (Jul 05 2018 at 19:37):

Use ulift empty instead of ulift.up empty. ulift.up is something you use on a term. On a type, you use simply ulift


Last updated: May 16 2021 at 21:11 UTC