Introduction to Univalent Foundations of Mathematics with Agda

Table of contents ⇑


We define our notation for type universes used in these notes, which is different from the standard Agda notation, but closer to the standard notation in HoTT/UF.

Readers unfamiliar with Agda should probably try to understand this only after doing some MLTT in Agda and HoTT/UF in 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 𝓀₁

The elements of Universe are universe names. Given a name 𝓀, the universe itself will be written 𝓀 Μ‡ Β  in these notes, with a deliberately almost invisible superscript dot.

We actually need to define this notation, because traditionally in Agda if one uses β„“ for a universe level, then Set β„“ is the type of types of level β„“. However, this notation is not good for univalent foundations, because not all types are sets. Also the terminology β€œlevel” is not good, because the hlevels in univalent type theory refer to the complexity of equality rather than size.

The following should be the only use of the Agda keyword Set in these notes.

Type = Ξ» β„“ β†’ Set β„“

_Μ‡   : (𝓀 : Universe) β†’ Type (𝓀 ⁺)

π“€β€ŠΜ‡  = Type 𝓀

This says that given the universe level 𝓀, we get the type universe π“€β€ŠΜ‡Β , which lives in the next next type universe universe 𝓀 ⁺. So the superscript dot notation is just a (postfix) synonym for (prefix) Type, which is just a synonym for Set, which means type in Agda.

We name a few of the initial universes:

𝓀₁ = 𝓀₀ ⁺
𝓀₂ = 𝓀₁ ⁺
𝓀₃ = 𝓀₂ ⁺

For notational convenience, we also define:

_⁺⁺ : Universe β†’ Universe
𝓀 ⁺⁺ = 𝓀 ⁺ ⁺

The following is sometimes useful:

universe-of : {𝓀 : Universe} (X : π“€βŸΜ‡ ) β†’ Universe
universe-of {𝓀} X = 𝓀


infix  1 _Μ‡

Table of contents ⇑