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