-- The Agda primitives (preloaded).
 
{-# OPTIONS --cubical-compatible --no-import-sorts --level-universe #-}
 
module Agda.Primitive where
 
------------------------------------------------------------------------
-- Universe levels
------------------------------------------------------------------------
 
infixl  _⊔_
 
{-# 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  _⊔_   #-}