On Universes in Lean

In this post, I'm explaining types, sorts and universes in Lean 4.

Type #n

You probably already know that this is how Lean types work:
"hi"          > String > Type > Type 1 > Type 2 > Type 3 > Type ~.
One other example is propositions:
2 + 2 = 4 > Prop  > Type > Type 1 > Type 2 > Type 3 > Type ~.
You might also know that Type is just syntax sugar for Type 0, overall it makes perfect sense.

Sorts and universes

What are universes, however, and what are sorts? It turns out, both are syntax sugar for some of the aforementioned entities.
Prop    is a syntax sugar for Sort 0,
Type 0 is a syntax sugar for Sort 1,
Type 1 is a syntax sugar for Sort 2,
Type 2 is a syntax sugar for Sort 3, etc.
Feel free to experiment with this by superseding every Prop you see by Sort 0, and every Type you see by Sort 1. I summed it up in the following table:

When we say "a particular universe" - we always refer to a particular Sort #n. That is, Sort 0, Sort 1, Sort 2,..., Type 0, Type 1, Type 2,..., Prop are all particular universes (some of them equivalent to each other), and there are no other universes in Lean.

Examples

The most simple and real-life example of where you might need to explicitly mention universes is when you want to create a list of types, for example [Nat, String, Int]. I assume here that you are vaguely familiar with the implementation of lists in Lean.
Your first attempt might look like this:

Now, the error makes sense, we're creating [Nat, Int, String], so our Nist has to accept α : Type 1. Let's try it:

Now, creating [Nat, Int, String] works, but we lost the ability to create ["red"]!

In general, to create a list [Type n, Type n, Type n], you need Fist to accept α : Type n + 2:

So how do we implement a list that would enable us to create  ["red", "green", "blue"], and [Nat, Int, String], and [Type 18, Type 18, Type 18]? We need Lean to determine the Type _ automatically, and this is achieved by declaring a universe: