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