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.
1Recall, from the Overture.Preliminaries module, the special notation we use to denote Agda’s levels and universes.