------------------------------------------------------------------------ -- Universe levels ------------------------------------------------------------------------ module Tools.Level where open import Agda.Primitive using (lzero; lsuc; Level; _⊔_) public ℓ₀ = lzero open import Level using (Lift; lift) public