Universe issue

Stream: maths

[Adam Topaz]

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?

[Chris B]

universe u

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

[Adam Topaz]

Why does one work and not the other?

[Chris B]

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.

[Reid Barton]

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

[Adam Topaz]

Ah! That makes more sense. Thank you!

[Adam Topaz]

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?

[Johan Commelin]

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.

[Reid Barton]

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

[Johan Commelin]

Oh, good point.

[Adam Topaz]

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