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 ℓ₀