Zulip Chat Archive

Stream: maths

Topic: Universe issue


view this post on Zulip Adam Topaz (Jul 09 2020 at 16:33):

I'm trying to define a dependent type inductively, but I'm running into some universe issues.
Here is a minimal example:

universe u
def foo :=   Type u

inductive bar (L : foo) :   Type u
| const {n : } : L n  bar n

/-
universe level of type_of(arg #3) of 'bar.const' is too big for the corresponding inductive datatype
-/

Is there another way to accomplish this?

view this post on Zulip Chris B (Jul 09 2020 at 17:42):

universe u

inductive bar (L :   Type u) :   Type u
| const {n : } : L n  bar n

view this post on Zulip Adam Topaz (Jul 09 2020 at 17:46):

Why does one work and not the other?

view this post on Zulip Chris B (Jul 09 2020 at 17:52):

def foo := nat -> Type u is a term with a value of nat -> Type u, so the type is something quantifying over Type u, therefore it needs to be greater than Type u. When you put (L : nat -> Type u) as a type parameter, you're saying "an element IN nat -> Type u".

I think the short answer that gets to what you probably meant to do is that def foo := nat -> Type u is not a type alias.

view this post on Zulip Reid Barton (Jul 09 2020 at 18:15):

The issue is really that the u is not the same. inductive bar (L : foo.{u}) works.

view this post on Zulip Adam Topaz (Jul 09 2020 at 18:16):

Ah! That makes more sense. Thank you!

view this post on Zulip Adam Topaz (Jul 09 2020 at 18:20):

So if I understand correctly it wasn't a type alias vs. def issue, but rather that when we write bar (L : ℕ → Type u) : ℕ → Type u the u is defined to be the same, so that's why inductive bar (L : foo.{u}) works (since we're explicitly setting the universe for foo to be u). Is that right?

view this post on Zulip Johan Commelin (Jul 09 2020 at 18:24):

I think lean could try to be smarter here. But I guess it's not very high priority on the list of things that can be improved.

view this post on Zulip Reid Barton (Jul 09 2020 at 18:29):

It also "works" (with a different meaning) with foo.{0} so I don't think it really makes sense to guess

view this post on Zulip Johan Commelin (Jul 09 2020 at 18:30):

Oh, good point.

view this post on Zulip Adam Topaz (Jul 09 2020 at 18:32):

Presumably lean could still figure out that a contraint that the universe of foo needs to be u\leq u (I know this doesn't really make sense in lean though).


Last updated: May 11 2021 at 16:22 UTC