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