## Stream: maths

### Topic: Universe issue

#### 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?

#### Chris B (Jul 09 2020 at 17:42):

universe u

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


#### Adam Topaz (Jul 09 2020 at 17:46):

Why does one work and not the other?

#### 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.

#### 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.

#### Adam Topaz (Jul 09 2020 at 18:16):

Ah! That makes more sense. Thank you!

#### 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?

#### 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.

#### 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

Oh, good point.

#### 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 $\leq u$ (I know this doesn't really make sense in lean though).

Last updated: May 11 2021 at 16:22 UTC