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

module Level where

infixl  _⊔_

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 {m n} (A : Set m) : Set (m ⊔ n) where
  constructor lift
  field lower : A

open Lift public