------------------------------------------------------------------------
-- The Agda standard library
--
-- Universe levels
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
module Level where
 
-- Levels.
 
open import Agda.Primitive as Prim public
  using    (Level; _⊔_; Setω)
  renaming (lzero to zero; lsuc to suc)
 
-- Lifting.
 
record Lift {a} ℓ (A : Set a) : Set (a ⊔ ℓ) where
  constructor lift
  field lower : A
 
open Lift public
 
-- Synonyms
 
0ℓ : Level
0ℓ = zero
 
levelOfType : ∀ {a} → Set a → Level
levelOfType {a} _ = a
 
levelOfTerm : ∀ {a} {A : Set a} → A → Level
levelOfTerm {a} _ = a