UniversePolymorphism

See the official user manual for the most up-to-date version of the information on this page.

TOC

Introduction to universes

Russell's paradox implies that the collection of all sets is not itself a set. Namely, if there were such a set U, then one could form the subset A ⊆ U of all sets that do not contain themselves. Then we would have A ∈ A if and only if A ∉ A, a contradiction.

For similar reasons, not every Agda type is a Set. For example, we have

 Bool : Set
 Nat : Set

but not Set : Set. However, it is often convenient for Set to have a type of its own, and so in Agda, it is given the type Set₁:

 Set : Set₁

In many ways, expressions of type Set₁ behave just like expressions of type Set; for example, they can be used as types of other things. However, the elements of Set₁ are potentially "larger"; when A : Set₁, then A is sometimes called a large set. In turn, we have

 Set₁ : Set₂
 Set₂ : Set₃

and so on. A type whose elements are types is called a universe; Agda provides an infinite number of universes Set, Set₁, Set₂, Set₃, ..., each of which is an element of the next one. In fact, Set itself is just an abbreviation for Set₀. The subscript n is called the level of the universe Setn.

A note on syntax: you can also write Set1, Set2, etc., instead of Set₁, Set₂. To enter a subscript in the Emacs mode, type "\_1".

Universe example

So why are universes useful? Because sometimes it is necessary to define, and prove theorems about, functions that operate not just on sets but on large sets. In fact, most Agda users sooner or later experience an error message where Agda complains that Set₁ != Set. These errors usually mean that a small set was used where a large one was expected, or vice versa.

For example, suppose you have defined the usual datatypes for lists and cartesian products:

 data List (A : Set) : Set where
   [] : List A
   _::_ : A -> List A -> List A

 data _×_ (A B : Set) : Set where
  _,_ : A -> B -> A × B

 infixr 5 _::_
 infixr 4 _,_
 infixr 2 _×_

Now suppose you would like to define an operator Prod that inputs a list of n sets and takes their cartesian product, like this:

 Prod (A :: B :: C :: []) = A × B × C 

There is only one small problem with this definition. The type of Prod should be

 Prod : List Set -> Set

However, the definition of List A specified that A had to be a Set. Therefore, List Set is not a valid type. The solution is to define a special version of the List operator that works for large sets:

 data List₁ (A : Set₁) : Set₁ where
   []₁ : List₁ A
   _::₁_ : A -> List₁ A -> List₁ A

With this, we can indeed define:

 Prod : List₁ Set -> Set
 Prod []₁ = Unit
 Prod (A ::₁ As) = A × Prod As

Universe polymorphism

Although we were able to give a type to the Prod operator by defining a special notion of large list, this quickly gets tiresome. Sooner or later, we find that we require yet another list type List₂, and it doesn't stop there. Also every function on lists (such as append) must be re-defined, and every theorem about such functions must be re-proved, for every possible level.

The solution to this problem is universe polymorphism. Agda provides a special primitive type Level, whose elements are possible levels of universes. In fact, the notation for the nth universe, Setn, is just an abbreviation for Set n, where n : Level is a level. We can use this to write a polymorphic List operator that works at any level. The library Agda.Primitive must be imported to access the Level type. The definition then looks like this:

 open import Agda.Primitive

 data List {n : Level} (A : Set n) : Set n where
   [] : List A
   _::_ : A -> List A -> List A

This new operator works at all levels; for example, we have

 List Nat : Set
 List Set : Set₁
 List Set₁ : Set₂

Level arithmetic

Even though we don't have the number of levels specified, we know that there is a lowest level lzero, and for each level n, there exists some higher level lsuc n; therefore, the set of levels is infinite. In addition, we can also take the least upper bound n ⊔ m of two levels. In summary, the following (and only the following) operations on levels are provided:

  lzero : Level
  lsuc  : (n : Level) → Level
  _⊔_   : (n m : Level) → Level

This is sufficient for most purposes; for example, we can define the cartesian product of two types of arbitrary (and not necessarily equal) levels like this:

 data _×_ {n m : Level} (A : Set n) (B : Set m) : Set (n ⊔ m) where
  _,_ : A -> B -> A × B

With this definition, we have, for example:

  Nat × Nat : Set
  Nat x Set : Set₁
  Set × Set : Set₁

∀-Notation

From the fact that we write Set n, it can always be inferred that n is a level. Therefore, when defining universe-polymorphic functions, it is common to use ∀-notation. For example, the type of the universe-polymorphic map operator on lists can be written

 map : ∀ {n m} {A : Set n} {B : Set m} → (A → B) → List A → List B

which is equivalent to

 map : {n m : Level} {A : Set n} {B : Set m} → (A → B) → List A → List B

Expressions of kind Setω

In a sense, universes were introduced to ensure that every Agda expression has a type, including expressions such as Set, Set₁, etc. However, the introduction of universe polymorphism inevitably breaks this property again, by creating some new terms that have no type. Consider the polymorphic singleton set Unit n : Setn, defined by

 data Unit (n : Level) : Set n where
   <> : Unit n

It is well-typed, and has type

 Unit : (n : Level) -> Set n

However, the type (n : Level) -> Set n, which is a valid Agda expression, does not belong to any universe. Indeed, the expression denotes a function mapping levels to universes, so if it had a type, it should be something like Level -> Universe, where Universe is the collection of all universes. But since the elements of Universe are types, Universe is itself a universe, so we have Universe : Universe. This leads to circularity and inconsistency. In other words, just as we cannot have a set of all sets, we also can't have a universe of all universes.

As a consequence, although the expression (n : Level) -> Set n is a type, it does not have a type. It does, however, have a "kind", which Agda calls Setω. There is no way to refer to Setω explicitly, but you may sometimes encounter it in error messages. For example, consider the following attempted definition:

 badSet : ?
 badSet = (n : Level) -> Set n

This results in the error message "Setω is not a valid type". For another example, consider trying to form the singleton list [ Unit ]:

 badList : List ((n : Level) -> Set n)
 badList = Unit :: []

This generates another error message about Setω. Again, the problem is that ((n : Level) -> Set n) does not belong to any universe, and therefore even the polymorphic List operator, which requires an argument of type Setn for some n, can't be applied to it. The only type constructor that can be applied to expressions of kind Setω is ->.

Installation or developer notes

• Universe polymorphism is now enabled by default. Use --no-universe-polymorphism to disable it.
• Universe levels are no longer defined as a data type. The level combinators are defined in ~/.cabal/share/<GHC-version>/<Agda-version>/lib/prim/Agda/Primitive.agda.
• The BUILTIN equality is now required to be universe-polymorphic.
• trustMe is now universe-polymorphic.