------------------------------------------------------------------------
-- Universe levels
------------------------------------------------------------------------

module Tools.Level where

open import Agda.Primitive using (lzero; lsuc; Level; _⊔_) public

ℓ₀ = lzero

open import Level using (Lift; lift) public