{-# 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 _̇