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.