------------------------------------------------------------------------
-- 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.

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

open Lift public