Checking my understanding of Lean's type theory

Stream: new members

[Noah Stebbins]

Hi guys :wave:

I'm new to Lean and wanted to check my understanding of a few concepts I read in Theorem Proving in Lean & played around with in VSCode.

Here's my understanding of #check Listbeing Type u → Type u

1. List takes in a parameter that specifies what the type of its members will be, e.g. ℕ, and returns a term of type List ℕ. In the ℕ case, we could think of List as Type 0 → Type 0
2. Furthermore, we want this hold for any type universe (e.g. Type 1, Type 2) not just Type 0. But we want to ensure that both the input and the output aren't within different universes but rather the same universe u, hence Type u → Type u. For the life of me I can't think of a case in which the type of the list would be in any universe other than 0. :thinking:

[Yaël Dillies]

1. Correct
2. That's not quite it. The underlying type theory forces List α to live in a universe at least as big as the one of α (think of it in terms of size. List α is at least as big as α since a ↦ [a] is an injection), and we make it live in the same universe out of simplicity. In fact, List : Type u → Type (max u v) would be perfectly allowed. A list of Type would have to live in Type 1 because Type : Type 1.