{-# OPTIONS --without-K --no-subtyping #-}
module Agda.Primitive where
infixl 6 _⊔_
postulate
Level : Set
{-# BUILTIN LEVEL Level #-}
postulate
lzero : Level
lsuc : (ℓ : Level) → Level
_⊔_ : (ℓ₁ ℓ₂ : Level) → Level
{-# BUILTIN LEVELZERO lzero #-}
{-# BUILTIN LEVELSUC lsuc #-}
{-# BUILTIN LEVELMAX _⊔_ #-}
{-# BUILTIN SETOMEGA Setω #-}