## Universes

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 _Μ
```