Universe levels in inductive types

Stream: general

[Julius Marozas]

Hi all,
I was playing around with the definition of a list:

inductive {u} list (α : Sort u) : Sort u
| nil : list
| cons : α → list → list

where #print list shows the following.

inductive list : Sort u → Sort u
constructors:
list.nil : Π {α : Sort u}, list α
list.cons : Π {α : Sort u}, α → list α → list α

So, I tried to redefine list without binding $\alpha$ (just like how #print shows it).

inductive {u} list : Sort u → Sort u
| nil : Π {α : Sort u}, list α
| cons : Π {α : Sort u}, α → list α → list α

But now I get an error: universe level of type_of(arg #1) of 'list.nil' is too big for the corresponding inductive datatype. I found that I can fix this by changing the type of list to be Sort u → Type u. But I am not sure why that's necessary, and why this doesn't break with the original definition.

[Kyle Miller]

@Julius Marozas The fix you found is equivalent to doing Sort u -> Sort (u + 1) (since Type u = Sort (u + 1) in general). Thinking about it in a computational way, the idea is that each constructor in an inductive type is expected to actually store its arguments so that you can later match and operate on them. Arguments to the type itself (the ones in the first line up to the colon) are not expected to be stored anywhere.

Your redefined list is one where each node keeps track of which type it's from, compared to the original where they don't. Recording types like this means the list must be in one universe higher -- otherwise list might be one of the types that can appear in one of the nodes, and impredicativity like that is not allowed ("predicativity" is that definitions can only ever refer to things that are defined before them; I guess the name "predicate" stuck, but only for one-argument Prop-valued functions).

Since each node knows the type of its element, you can easily go to fully heterogeneous lists, though there's not much you can really do with a list like this other than compute its length:

inductive {u} list : Sort (u+1)
| nil : list
| cons : Π {α : Sort u}, α → list → list

[Eric Wieser]

That's isomorphic to list (sigma $ @id (Sort u)), right?

[Julius Marozas]

@Kyle Miller Thanks for the explanation, it's much clearer now.
@Eric Wieser The code you provided doesn't seem to type check, maybe you meant this: list (sigma $ @id (Sort (u + 1)))?

[Eric Wieser]

Oh, I forgot that I wasn't allowed to put sorts in a list or sigma type

[Eric Wieser]

I might also mean list (sigma $ @id (Type u)) or list (psigma $ @id (Sort u))

[Julius Marozas]

Yeah, that seems to work. What's the point of having both psigma and sigma?

[Eric Wieser]

psigma causes annoying universe elaboration issues, apparently

[Eric Wieser]

Which aren't worth sufferring through for 90% of the cases when you know you only are dealing with Types

[Julius Marozas]

Interesting, do you have any examples of such cases, or documentation on this topic?

[Eric Wieser]

It would be great if someone could add a library note for this, so we could reference it from psigma and pprod

[Yaël Dillies]

I already hint at it in the module docs of data.sigma.basic