# 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.