{-# OPTIONS --without-K --safe #-}

module Tools.Level where

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

ℓ₀ = lzero

open import Level using (Lift; lift) public