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 = π€

Fixities:

infix 1 _Μ