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