Universe Levels

Agda’ type system includes an infinite hierarchy of universes Setᵢ : Setᵢ₊₁. This hierarchy enables quantification over arbitrary types without running into the inconsistency that follows from Set : Set. These universes are further detailed on the page on Agda’s sort system.

However, when working with this hierarchy it can quickly get tiresome to repeat the same definition at different universe levels. For example, we might be forced to define new datatypes data List (A : Set) : Set, data List₁ (A : Set₁) : Set₁, etc. 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 n th universe, Setₙ, 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₁

Intrinsic level properties

Levels and their associated operations have some properties which are internally and automatically solved by the compiler. This means that we can replace some expressions with others, without worrying about the expressions for their corresponding levels matching exactly.

For example, we can write:

_ : {F : (l : Level) → Set l} {l1 l2 : Level} → F (l1 ⊔ l2) → F (l2 ⊔ l1)
_ = λ x → x

and Agda does the conversion from F (l1 ⊔ l2) to F (l2 ⊔ l1) automatically.

Here is a list of the level properties:

• Idempotence: a ⊔ a is the same as a.

• Associativity: (a ⊔ b) ⊔ c is the same as a ⊔ (b ⊔ c).

• Commutativity: a ⊔ b is the same as b ⊔ a.

• Distributivity of lsuc over ⊔: lsuc (a ⊔ b) is the same as lsuc a ⊔ lsuc b.

• Neutrality of lzero: a ⊔ lzero is the same as a.

• Subsumption: a ⊔ lsuc a is the same as lsuc a. Notably, this also holds for arbitrarily many lsuc usages: a ⊔ lsuc (lsuc a) is also the same as lsuc (lsuc a).

forall 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 the ∀ (or forall) 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 sort 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 : Setₙ, 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 in the Set hierarchy. Indeed, the expression denotes a function mapping levels to sorts, so if it had a type, it should be something like Level → Sort, where Sort is the collection of all sorts. But if Agda were to support a sort Sort of all sorts, it would be a sort itself, so in particular we would have Sort : Sort. Just like Type : Type, this would leads to circularity and inconsistency.

Instead, Agda introduces a new sort Setω that stands above all sorts Set ℓ, but is not itself part of the hierarchy. For example, Agda assigns the expression (n : Level) → Set n to be of type Setω.

Setω is itself the first step in another infinite hierarchy Setωᵢ : Setωᵢ₊₁. However, this hierarchy does not support universe polymorphism, i.e. there are no sorts Setω ℓ for ℓ : Level. Allowing this would require a new universe Set2ω, which would then naturally lead to Set2ω₁, and so on. Disallowing universe polymorphism for Setωᵢ avoids the need for such even larger sorts. This is an intentional design decision.

Pragmas and options

• The option --type-in-type disables the checking of universe level consistency for the whole file.

• The option --omega-in-omega enables the typing rule Setω : Setω (thus making Agda inconsistent) but otherwise leaves universe checks intact.

• The pragma {-# NO_UNIVERSE_CHECK #-} can be put in front of a data or record type to disable universe consistency checking locally. Example:

  {-# NO_UNIVERSE_CHECK #-}
  data U : Set where
    el : Set → U

  This pragma applies only to the check that the universe level of the type of each constructor argument is less than or equal to the universe level of the datatype, not to any other checks.

  New in version 2.6.0.

The options --type-in-type and --omega-in-omega and the pragma {-# NO_UNIVERSE_CHECK #-} cannot be used with –safe.