Cumulativity

Basics

Since version 2.6.1, Agda supports optional cumulativity of universes under the --cumulativity flag.

{-# OPTIONS --cumulativity #-}

When the --cumulativity flag is enabled, Agda uses the subtyping rule Set i =< Set j whenever i =< j. For example, in addition to its usual type Set, Nat also has the type Set₁ and even Set i for any i : Level.

_ : Set
_ = Nat
_ : Set₁
_ = Nat
_ : ∀ {i} → Set i
_ = Nat

With cumulativity is enabled, one can implement lifting to a higher universe as the identity function.

lift : ∀ {a b} → Set a → Set (a ⊔ b)
lift x = x

Example usage: N-ary functions

In Agda without cumulativity, it is tricky to define a universe-polymorphic N-ary function type A → A → ... → A → B because the universe level depends on whether the number of arguments is zero:

module Without-Cumulativity where
  N-ary-level : Level → Level → Nat → Level
  N-ary-level ℓ₁ ℓ₂ zero    = ℓ₂
  N-ary-level ℓ₁ ℓ₂ (suc n) = ℓ₁ ⊔ N-ary-level ℓ₁ ℓ₂ n
  N-ary : ∀ {ℓ₁ ℓ₂} n → Set ℓ₁ → Set ℓ₂ → Set (N-ary-level ℓ₁ ℓ₂ n)
  N-ary zero    A B = B
  N-ary (suc n) A B = A → N-ary n A B

In contrast, in Agda with cumulativity one can always work with the highest possible universe level. This makes it much easier to define the type of N-ary functions.

module With-Cumulativity where
  N-ary : Nat → Set ℓ₁ → Set ℓ₂ → Set (ℓ₁ ⊔ ℓ₂)
  N-ary zero    A B = B
  N-ary (suc n) A B = A → N-ary n A B
  curryⁿ : (Vec A n → B) → N-ary n A B
  curryⁿ {n = zero}  f = f []
  curryⁿ {n = suc n} f = λ x → curryⁿ λ xs → f (x ∷ xs)
  _$ⁿ_ : N-ary n A B → (Vec A n → B)
  f $ⁿ []       = f
  f $ⁿ (x ∷ xs) = f x $ⁿ xs
  ∀ⁿ : ∀ {A : Set ℓ₁} n → N-ary n A (Set ℓ₂) → Set (ℓ₁ ⊔ ℓ₂)
  ∀ⁿ zero    P = P
  ∀ⁿ (suc n) P = ∀ x → ∀ⁿ n (P x)

Limitations

Currently cumulativity only enables subtyping between universes, but not between any other types containing universes. For example, List Set is not a subtype of List Set₁. Agda also does not have cumulativity for any other types containing universe levels, so List {lzero} Nat is not a subtype of List {lsuc lzero} Nat. Such rules might be added in a future version of Agda.

Constraint solving

When working in Agda with cumulativity, universe level metavariables are often underconstrained. For example, the expression List Nat could mean List {lzero} Nat, but also List {lsuc lzero} Nat, or indeed List {i} Nat for any i : Level.

Currently Agda uses the following heuristic to instantiate universe level metavariables. At the end of each type signature, each mutual block, or declaration that is not part of a mutual block, Agda instantiates all universe level metavariables that are unbounded from above. A metavariable _l : Level is unbounded from above if all unsolved constraints that mention the metavariable are of the form aᵢ =< _l : Level, and _l does not occur in the type of any other unsolved metavariables. For each metavariable that satisfies these conditions, it is instantiated to a₁ ⊔ a₂ ⊔ ... ⊔ aₙ where a₁ =< _l : Level, …, aₙ =< _l : Level are all constraints that mention _l.

The heuristic as described above is considered experimental and is subject to change in future versions of Agda.