This is the Overture.Lifts module of the Agda Universal Algebra Library.

{-# OPTIONS --without-K --exact-split --safe #-} module Overture.Lifts where open import Overture.Inverses public

The hierarchy of universes in Agda is structured as follows:^{1}

```
𝓤 ̇ : 𝓤 ⁺ ̇, 𝓤 ⁺ ̇ : 𝓤 ⁺ ⁺ ̇, etc.
```

This means that the universe `𝓤 ̇`

has type `𝓤 ⁺ ̇`

, and `𝓤 ⁺ ̇`

has type `𝓤 ⁺ ⁺ ̇`

, and so on. It is important to note, however, this does *not* imply that `𝓤 ̇ : 𝓤 ⁺ ⁺ ̇`

. In other words, Agda’s universe hierarchy is *noncumulative*. This makes it possible to treat universe levels more generally and precisely, which is nice. On the other hand, a noncumulative hierarchy can sometimes make for a nonfun proof assistant. Specifically, in certain situations, the noncumulativity makes it unduly difficult to convince Agda that a program or proof is correct.

Here we describe a general `Lift`

type that help us overcome the technical issue described in the previous subsection. In the Lifts of algebras section of the Algebras.Algebras module we will define a couple domain-specific lifting types which have certain properties that make them useful for resolving universe level problems when working with algebra types.

Let us be more concrete about what is at issue here by considering a typical example. Agda will often complain with errors like the following:

`
Birkhoff.lagda:498,20-23
𝓤 != 𝓞 ⊔ 𝓥 ⊔ (𝓤 ⁺) when checking that the expression... has type...
`

This error message means that Agda encountered the universe level `𝓤 ⁺`

, on line 498 (columns 20–23) of the file `Birkhoff.lagda`

, but was expecting a type at level `𝓞 ⁺ ⊔ 𝓥 ⁺ ⊔ 𝓤 ⁺ ⁺`

instead.

The general `Lift`

record type that we now describe makes these situations easier to deal with. It takes a type inhabiting some universe and embeds it into a higher universe and, apart from syntax and notation, it is equivalent to the `Lift`

type one finds in the `Level`

module of the Agda Standard Library.

record Lift {𝓦 𝓤 : Universe} (A : 𝓤 ̇) : 𝓤 ⊔ 𝓦 ̇ where constructor lift field lower : A open Lift

The point of having a ramified hierarchy of universes is to avoid Russell’s paradox, and this would be subverted if we were to lower the universe of a type that wasn’t previously lifted. However, we can prove that if an application of `lower`

is immediately followed by an application of `lift`

, then the result is the identity transformation. Similarly, `lift`

followed by `lower`

is the identity.

lift∼lower : {𝓦 𝓤 : Universe}{A : 𝓤 ̇} → lift ∘ lower ≡ 𝑖𝑑 (Lift{𝓦} A) lift∼lower = refl lower∼lift : {𝓦 𝓤 : Universe}{A : 𝓤 ̇} → lower{𝓦}{𝓤} ∘ lift ≡ 𝑖𝑑 A lower∼lift = refl

The proofs are trivial. Nonetheless, we’ll come across some holes these lemmas can fill.

^{1}Recall, from the Overture.Preliminaries module, the special notation we use to denote Agda’s *levels* and *universes*.