------------------------------------------------------------------------
-- Universe levels
------------------------------------------------------------------------

{-# OPTIONS --universe-polymorphism #-}

module Level where

-- Levels.

infixl 6 _⊔_

postulate
  Level : Set
  zero  : Level
  suc   : Level  Level
  _⊔_   : Level  Level  Level

-- MAlonzo compiles Level to (). This should be safe, because it is
-- not possible to pattern match on levels.

{-# COMPILED_TYPE Level ()     #-}
{-# COMPILED zero ()           #-}
{-# COMPILED suc  (\_ -> ())   #-}
{-# COMPILED _⊔_  (\_ _ -> ()) #-}

{-# BUILTIN LEVEL     Level #-}
{-# BUILTIN LEVELZERO zero  #-}
{-# BUILTIN LEVELSUC  suc   #-}
{-# BUILTIN LEVELMAX  _⊔_   #-}

-- Lifting.

record Lift {a } (A : Set a) : Set (a  ) where
  constructor lift
  field lower : A

open Lift public