------------------------------------------------------------------------
-- 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
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4