{-# OPTIONS --cubical-compatible --no-import-sorts --level-universe #-}
module Agda.Primitive where
infixl 6 _⊔_
{-# BUILTIN PROP Prop #-}
{-# BUILTIN TYPE Set #-}
{-# BUILTIN STRICTSET SSet #-}
{-# BUILTIN PROPOMEGA Propω #-}
{-# BUILTIN SETOMEGA Setω #-}
{-# BUILTIN STRICTSETOMEGA SSetω #-}
{-# BUILTIN LEVELUNIV LevelUniv #-}
postulate
Level : LevelUniv
{-# BUILTIN LEVEL Level #-}
postulate
lzero : Level
lsuc : (ℓ : Level) → Level
_⊔_ : (ℓ₁ ℓ₂ : Level) → Level
{-# BUILTIN LEVELZERO lzero #-}
{-# BUILTIN LEVELSUC lsuc #-}
{-# BUILTIN LEVELMAX _⊔_ #-}