Source code on Github
------------------------------------------------------------------------
-- 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