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