Sort System

Sorts (also known as universes) are types whose members themselves are again types. The fundamental sort in Agda is named Type and it denotes the universe of small types. But for some applications, other sorts are needed. This page explains the need for additional sorts and describes all the sorts that are used by Agda.

The theoretical foundation for Agda’s sort system are Pure Type Systems (PTS). A PTS has, besides the set of supported sorts, two parameters:

1. A set of axioms of the form s : s′, stating that sort s itself has sort s′.

2. A set of rules of the form (s₁, s₂, s₃) stating that if A : s₁ and B(x) : s₂ then (x : A) → B(x) : s₃.

Agda is a functional PTS in the sense that s₃ is uniquely determined by s₁ and s₂. Axioms are implemented internally by the univSort function, see univSort. Rules are implemented by the funSort and piSort functions, see funSort.

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.

Likewise, Martin-Löf’s type theory had originally a rule Type : Type but Girard showed that it is inconsistent. This result is known as Girard’s paradox. Hence, not every Agda type is a Type. For example, we have

Bool : Type
Nat  : Type

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

Type : Type₁

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

Type₁ : Type₂
Type₂ : Type₃

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

Note

You can also write Type1, Type2, etc., instead of Type₁, Type₂. 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 types but on large types. In fact, most Agda users sooner or later experience an error message where Agda complains that Type₁ != Type. These errors usually mean that a small type 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 : Type) : Type where
  [] : List A
  _::_ : A → List A → List A

data _×_ (A B : Type) : Type 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 types and outputs 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 Type → Type

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

data List₁ (A : Type₁) : Type₁ where
  []   : List₁ A
  _::_ : A → List₁ A → List₁ A

With this, we can indeed define:

Prod : List₁ Type → Type
Prod []        = ⊤
Prod (A :: As) = A × Prod As

Universe polymorphism

To allow definitions of functions and datatypes that work for all possible universes Typeᵢ, Agda provides a type Level of universe levels and level-polymorphic universes Type ℓ where ℓ : Level. For more information, see the page on universe levels.

Agda’s sort system

The implementation of Agda’s sort system is based on the theory of pure type systems. The full sort system of Agda consists of the following sorts:

1. Standard small sorts (universe-polymorphic).

   • Typeᵢ and its universe-polymorphic variant Type ℓ

   • Propᵢ and its universe-polymorphic variant Prop ℓ (with --prop)

   • SSetᵢ and its universe-polymorphic variant SSet ℓ (with --two-level)

2. Standard large sorts (non polymorphic).

   • Typeωᵢ

   • Propωᵢ (with --prop)

   • SSetωᵢ (with --two-level)

3. Special sorts.

   • IUniv, short for interval universe (with --cubical)

   • LevelUniv (with --level-universe)

Only the small standard sort hierarchies Type and Prop are in scope by default (see --import-sorts). They and most other sorts are defined in the system module Agda.Primitive. Sorts, even though they might enjoy the priviledge of numeric suffixes, are brought into scope just as any Agda definition, by open Agda.Primitive. Note that sorts can also be renamed, e.g., open Agda.Primitive renaming (Type to Kind).

Some special sorts are defined in other system modules, see Special sorts.

Sorts Typeᵢ and Type ℓ

As explained in the introduction, Agda has a hierarchy of sorts Typeᵢ : Typeᵢ₊₁, where i is any concrete natural number, i.e. 0, 1, 2, 3, … The sort Type is an abbreviation for Type₀.

You can also refer to these sorts with the alternative syntax Typei. That means that you can also write Type0, Type1, Type2, etc., instead of Type₀, Type₁, Type₂.

In addition, Agda supports the universe-polymorphic version Type ℓ where ℓ : Level (see universe levels).

Sorts Propᵢ and Prop ℓ

In addition to the hierarchy Typeᵢ, Agda also supports a second hierarchy Propᵢ : Typeᵢ₊₁ (or Propi) of proof-irrelevant propositions. Like Type, Prop also has a universe-polymorphic version Prop ℓ where ℓ : Level.

Sorts SSetᵢ and SSet ℓ

These experimental universes SSet₀ : SSet₁ : SSet₂ : ... of strict sets or non-fibrant sets are described in Two-Level Type Theory.

Sorts Typeωᵢ

To assign a sort to types such as (ℓ : Level) → Type ℓ, Agda further supports an additional sort Typeω that stands above all sorts Typeᵢ.

Just as for Type and Prop, Typeω is the lowest level at an infinite hierarchy Typeωᵢ : Typeωᵢ₊₁ where Typeω = Typeω₀. You can also refer to these sorts with the alternative syntax Typeωi. That means that you can also write Typeω0, Typeω1, Typeω2, etc., instead of Typeω₀, Typeω₁, Typeω₂.

However, unlike the standard hierarchy of universes Typeᵢ, the second hierarchy Typeωᵢ does not support universe polymorphism. This means that it is not possible to quantify over all Typeωᵢ at once. For example, the expression ∀ {i} (A : Typeω i) → A → A would not be a well-formed agda term. See the section on Typeω on the page on universe levels for more information.

Concerning other applications, it should not be necessary to refer to these sorts during normal usage of Agda, but they might be useful for defining reflection-based macros. And it is allowed to define data types in Typeωᵢ.

Note

When --omega-in-omega is enabled, Typeωᵢ is considered to be equal to Typeω for all i (thus rendering Agda inconsistent).

Sorts Propωᵢ

This transfinite extension of the Prop hierarchy works analogous to Typeωᵢ. However, it is not motivated by typing (ℓ : Level) → Prop ℓ, because that lives in Typeω. Instead, it may be used to host large inductive propositions, where constructors can have fields that live at any finite level ℓ.

The sorting rules for finite levels extend to the transfinite hierarchy, so we have Propωᵢ : Typeωᵢ₊₁.

Sorts SSetωᵢ

This is a transfinite extension of the SSet hierarchy.

Special sorts

Special sorts host special types that are not placed in a standard universe for technical reasons, typically because they require special laws for function type formation (see funSort).

With --cubical and open import Agda.Primitive.Cubical we get IUniv which hosts the interval I.

With --level-universe the type Level no longer lives in Type but in its own sort LevelUniv. It is still defined in Agda.Primitive.

Sort metavariables and unknown sorts

Under universe polymorphism, levels can be arbitrary terms, e.g., a level that contains free variables. Sometimes, we will have to check that some expression has a valid type without knowing what sort it has. For this reason, Agda’s internal representation of sorts implements a constructor (sort metavariable) representing an unknown sort. The constraint solver can compute these sort metavariables, just like it does when computing regular term metavariables.

However, the presence of sort metavariables also means that sorts of other types can sometimes not be computed directly. For this reason, Agda’s internal representation of sorts includes three additional constructors univSort, funSort, and piSort. These constructors compute to the proper sort once enough metavariables in their arguments have been solved.

Note

univSort, funSort and piSort are internal constructors that may be printed when evaluating a term. The user cannot enter them, nor introduce them in Agda code. All these constructors do not represent new sorts but instead, they compute to the right sort once their arguments are known.

univSort

univSort returns the successor sort of a given sort. In PTS terminology, it implements the axioms s : univSort s.

univSort

sort	successor sort
Prop a	Prop (lsuc a)
Type a	Type (lsuc a)
SSet a	SSet (lsuc a)
Propωᵢ	Propωᵢ₊₁
Typeωᵢ	Typeωᵢ₊₁
SSetωᵢ	SSetωᵢ₊₁
IUniv	SSet₁
LockUniv	Type₁
LevelUniv	Type₁
_1	univSort _1

funSort

The constructor funSort computes the sort of a function type even if the sort of the domain and the sort of the codomain are still unknown.

To understand how funSort works in general, let us assume the following scenario:

• sA and sB are two (possibly different) sorts.

• A : sA, meaning that A is a type that has sort sA.

• B : sB, meaning that B is a (possibly different) type that has sort sB.

Under these conditions, we can build the function type A → B : funSort sA sB. This type signature means that the function type A → B has a (possibly unknown) but well-defined sort funSort sA sB, specified in terms of the sorts of its domain and codomain.

Example: the sort of the function type ∀ {A} → A → A with normal form {A : _5} → A → A evaluates to funSort (univSort _5) (funSort _5 _5) where:

• _5 is a metavariable that represents the sort of A.

• funSort _5 _5 is the sort of A → A.

If sA and sB happen to be known, then funSort sA sB can be computed to a sort value.

To specify how funSort computes, let U range over Prop, Type, SSet and let U ↝ U' be SSet if one of U, U' is SSet, and U' otherwise. E.g. SSet ↝ Prop is SSet and Type ↝ Prop is Prop. Also, let L range over levels a and transfinite numbers ωᵢ (which is ω + i) and let us generalize ⊔ to L ⊔ L', e.g. a ⊔ ωᵢ = ωᵢ and ωᵢ ⊔ ωⱼ = ωₖ where k = max i j. We write standard universes as pairs U L, e.g. Propωᵢ as pair Prop ωᵢ. Let S range over special universes IUniv, LockUniv, LevelUniv.

In the following table we specify how funSort s₁ s₂ computes on known sorts s₁ and s₂, excluding interactions between different special sorts. In PTS terminology, these are the rules (s₁, s₂, funSort s₁ s₂).

funSort

s₁	s₂	funSort s₁ s₂
U L	U' L'	(U ↝ U') (L ⊔ L')
U L	IUniv	SSet L
U ωᵢ	S ≠ IUniv	Type ωᵢ
S	U ωᵢ	U ωᵢ
S ≠ LevelUniv	U a	U a
LevelUniv	U a	U ω₀
LevelUniv	LevelUniv	LevelUniv
IUniv	IUniv	SSet₀

Here are some examples for the standard universes U L:

funSort Typeωᵢ   Typeωⱼ   = Typeωₖ            (where k = max(i,j))
funSort Typeωᵢ   (Type b) = Typeωᵢ
funSort Typeωᵢ   (Prop b) = Typeωᵢ
funSort (Type a) Typeωⱼ   = Typeωⱼ
funSort (Prop a) Typeωⱼ   = Typeωⱼ
funSort (Type a) (Type b) = Type (a ⊔ b)
funSort (Prop a) (Type b) = Type (a ⊔ b)
funSort (Type a) (Prop b) = Prop (a ⊔ b)
funSort (Prop a) (Prop b) = Prop (a ⊔ b)

Note

funSort can admit just two arguments, so it will be iterated when the function type has multiple arguments. E.g. the function type ∀ {A} → A → A → A evaluates to funSort (univSort _5) (funSort _5 (funSort _5 _5))

piSort

Similarly, piSort s1 (λ x → s2) is a more general version of funSort that computes the sort of a Π-type given the sort s1 of its domain and the sort s2 of its codomain as arguments. It is used in cases where the sort of the codomain of a Π-type might be dependent on the variable bound by the Π-type. It computes to either funSort (when the codomain sort is not dependent) or to Typeω (when it is dependent).

To understand how piSort works in general, we set the following scenario:

• sA and sB are two (possibly different) sorts.

• A : sA, meaning that A is a type that has sort sA.

• x : A, meaning that x has type A.

• B : sB, meaning that B is a type (possibly different than A) that has sort sB.

Under these conditions, we can build the dependent function type (x : A) → B : piSort sA (λ x → sB). This type signature means that the dependent function type (x : A) → B has a (possibly unknown) but well-defined sort piSort sA (λ x → sB), specified in terms of the sorts of its domain and codomain.

Here are some examples how piSort computes:

piSort s1       (λ x → s2)    = funSort s1 s2          (if x does not occur freely in s2)
piSort (Type ℓ)  (λ x → Type ℓ') = Typeω                  (if x occurs rigidly in ℓ')
piSort (Prop ℓ) (λ x → Type ℓ') = Typeω                  (if x occurs rigidly in ℓ')
piSort Typeωᵢ    (λ x → Type ℓ') = Typeωᵢ                 (if x occurs rigidly in ℓ')

With these rules, we can compute the sort of the function type ∀ {A} → ∀ {B} → B → A → B (or more explicitly, {A : _9} {B : _7} → B → A → B) to be piSort (univSort _9) (λ A → funSort (univSort _7) (funSort _7 (funSort _9 _7))).

More examples:

• piSort LevelUniv (λ l → Type l) evaluates to Typeω (see also level universe)

• piSort (Type l) (λ _ → Type l') evaluates to Type (l ⊔ l')

• piSort s (λ _ → Typeωi) evaluates to funSort s Typeωi