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.

Each entity in red is a Lean universe

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:

Application type mismatch: argument has type Type 1
but is expected to have type Type

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

Application type mismatch: argument has type Type
but is expected to have type Type 1

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:

You can't change any of these numbers, they should all be smaller than the prior one by 1.

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:

A direct copy of Lean's definition of a List.