31 lines
924 B
Agda
31 lines
924 B
Agda
|
{-# OPTIONS --without-K --exact-split --safe --auto-inline #-}
|
|||
|
|
|
|||
|
|
module Universes where
|
|||
|
|
|
|||
|
|
open import Agda.Primitive public
|
|||
|
|
renaming (
|
|||
|
|
Level to Universe -- We speak of universes rather than of levels.
|
|||
|
|
; lzero to 𝓤₀ -- Our first universe is called 𝓤₀
|
|||
|
|
; lsuc to _⁺ -- The universe after 𝓤 is 𝓤 ⁺
|
|||
|
|
; Setω to 𝓤ω -- There is a universe 𝓤ω strictly above 𝓤₀, 𝓤₁, ⋯ , 𝓤ₙ, ⋯
|
|||
|
|
)
|
|||
|
|
using (_⊔_) -- Least upper bound of two universes, e.g. 𝓤₀ ⊔ 𝓤₁ is 𝓤₁
|
|||
|
|
|
|||
|
|
Type = λ ℓ → Set ℓ
|
|||
|
|
|
|||
|
|
_̇ : (𝓤 : Universe) → Type (𝓤 ⁺)
|
|||
|
|
|
|||
|
|
𝓤 ̇ = Type 𝓤
|
|||
|
|
|
|||
|
|
𝓤₁ = 𝓤₀ ⁺
|
|||
|
|
𝓤₂ = 𝓤₁ ⁺
|
|||
|
|
𝓤₃ = 𝓤₂ ⁺
|
|||
|
|
|
|||
|
|
_⁺⁺ : Universe → Universe
|
|||
|
|
𝓤 ⁺⁺ = 𝓤 ⁺ ⁺
|
|||
|
|
|
|||
|
|
universe-of : {𝓤 : Universe} (X : 𝓤 ̇ ) → Universe
|
|||
|
|
universe-of {𝓤} X = 𝓤
|
|||
|
|
|
|||
|
|
infix 1 _̇
|