In this post, I'm explaining types, sorts and universes in Lean 4.
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.
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,
Prop are all particular universes (some of them equivalent to each other), and there are no other universes in Lean.
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:
[Nat, Int, String] works, but we lost the ability to create
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: