module Level where open import Agda.Primitive public -- Lifting record Lift {ℓ ℓ' : Level} (A : Set ℓ) : Set (ℓ ⊔ ℓ') where constructor lift field lower : A open Lift public -- level zero ℓ₀ : Level ℓ₀ = lzero -- level one ℓ₁ : Level ℓ₁ = lsuc ℓ₀