Types, Sorts, and Universes in Lean 4

Types

You probably already know that this is how Lean types work:
"hi" > String > Type 0 > Type 1 > Type 2 > Type 3 > . . . 

Or, for propositions:
2 + 2 = 4 > Prop > Type 0 > Type 1 > Type 2 > Type 3 > . . .

This can be displayed in a table as follows:

Syntax sugar: Sorts and Universes

Lean introduces some syntax sugar for some values defined above - so called Sorts.

Sort 0 is a syntax sugar for Prop,
Sort 1 is a syntax sugar for Type 0,
Sort 2 is a syntax sugar for Type 1,
Sort 3 is a syntax sugar for Type 2, etc.

Additionally, Type is syntax sugar for Type 0.

You can see from the table above that this sugaring is sort of asymmetrical. The only value from the String/Nat/Prop column that's considered a sort is a Prop.

So, if we were to highlight all sorts in our table, it would look as follows:

Or, syntax-sugared:

When we refer to "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.

Example

Suppose you want to implement Lists in Lean.
And suppose you want your List implementation to handle various lists, say def myListOfStrings = ["red", "green", "blue"] , or  def myListOfTypes := [Nat, String, Int]. 

First attempt

Your first attempt might look like this:

inductive Nist (α : Type 0) where
| nil
| cons (head : α) (tail : Nist α)

def strings : Nist String   := Nist.cons "red" Nist.nil
def types   : Nist (Type 0) := Nist.cons Nat Nist.nil   -- ERROR: "Type 0" gets underlined!

This will get you the following error: "Application type mismatch: argument has type Type 1 but is expected to have type Type 0".
Notice that Lean is complaining about the argument we pass to Nist ourArgument (imagine inductives as function that can be called).
After some deliberation, you will come to the conclusion that this error makes sense: Nist (Type 0) line would only work if the type of Type 0 was Type 0, which we know is not the case from the table in the beginning of the article.

Second attempt

Okay, so we understood that Nist (α : Type 0) cannot handle a list of types, let's change it to Cist (α : Type 1):

inductive Cist (α : Type 1) where
| nil
| cons (head : α) (tail : Cist α)

def strings : Cist String   := Cist.cons "red" Cist.nil -- ERROR: "String" gets underlined!
def types   : Cist (Type 0) := Cist.cons Nat Cist.nil   

Great, our list of types works now!
However now the list of strings errors out with "Application type mismatch: argument has type Type 0 but is expected to have type Type 1". We lost the ability to create a simple list of strings!

Third attempt

Clearly, it's impossible to implement a List that will be able to handle any kind of types just by changing the #NUMBER in inductive List (α : Type #NUMBER). The least we can do is notice a pattern: to create a list [Type n, Type n, Type n], you need your list to accept α : Type n + 2:

inductive Fist (α : Type 20) where
| nil
| cons (head : α) (tail : Fist α)

def types : Fist (Type 19) := Fist.cons (Type 18) Fist.nil

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

Solution

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:

universe u

inductive List (α : Type u) where
| nil
| cons (head : α) (tail : List α)

def a : List String := ["red", "green", "blue"]
def b : List (Type 0) := [Nat, String, Int]
def c : List (Type 19) := [Type 18, Type 18, Type 18]

As it happens this is a direct copy of Lean's definition of a List!

Summary

Sorts and universes are exactly the same thing.

A sort is everything that starts with Type #n, plus, as a single exception, Prop.

universe u is a handy way to avoid creating inductive Nist (α : Type 0),  inductive Cist (α : Type 1), inductive Fist (α : Type 20), . . .  per each list we might want to create. With universes, we can simply ask Lean to derive the Type #n we want per each partciular list of ours by writing inductive List (α : Type u).