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