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

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

module Level where

-- Levels.

data Level : Set where
  zero : Level
  suc  : (i : Level)  Level

{-# BUILTIN LEVEL     Level #-}
{-# BUILTIN LEVELZERO zero  #-}
{-# BUILTIN LEVELSUC  suc   #-}

-- Maximum.

infixl 6 _⊔_

_⊔_ : Level  Level  Level
zero   j     = j
suc i  zero  = suc i
suc i  suc j = suc (i  j)

{-# BUILTIN LEVELMAX _⊔_ #-}

-- Lifting.

data Lift {a } (A : Set a) : Set (a  ) where
  lift : (x : A)  Lift A