-- The Agda primitives (preloaded). {-# OPTIONS --cubical-compatible --no-import-sorts --level-universe #-} module Agda.Primitive where ------------------------------------------------------------------------ -- Universe levels ------------------------------------------------------------------------ infixl 6 _⊔_ {-# BUILTIN PROP Prop #-} {-# BUILTIN TYPE Set #-} {-# BUILTIN STRICTSET SSet #-} {-# BUILTIN PROPOMEGA Propω #-} {-# BUILTIN SETOMEGA Setω #-} {-# BUILTIN STRICTSETOMEGA SSetω #-} {-# BUILTIN LEVELUNIV LevelUniv #-} -- Level is the first thing we need to define. -- The other postulates can only be checked if built-in Level is known. postulate Level : LevelUniv -- MAlonzo compiles Level to (). This should be safe, because it is -- not possible to pattern match on levels. {-# BUILTIN LEVEL Level #-} postulate lzero : Level lsuc : (ℓ : Level) → Level _⊔_ : (ℓ₁ ℓ₂ : Level) → Level {-# BUILTIN LEVELZERO lzero #-} {-# BUILTIN LEVELSUC lsuc #-} {-# BUILTIN LEVELMAX _⊔_ #-}