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, 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.
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: