```
module Types.universe where
open import Lang.dataStructures using (
Bool; true; false;
⊥; ⊤; ℕ; List;
zero; one)
open import Agda.Primitive renaming (
Level to AgdaLevel;
lzero to alzero;
lsuc to alsuc;
_⊔_ to _⊔⊔_)
```

A universe can be thought of as a container for all of mathematics. There is no mathematics that is possible outside of universe. Now obviously this differs from our physical universe in a way that mathematics also describes purely conceptual stuff that need not have a physical manifestation, rather, in many ways our univrerse is a subset of the mathematical universe as it can be described by mathematical models.

For set theory, the universe can be thought as the set of all sets. For type theory, universes contain all types - hence essentially everything including objects, laws, theorems etc. The structure of the universe used in type theory are Russel-style and Taski-style universes though we use the former as it is easier and sufficient for our purposes. There are other kinds of universes in mathematics, for example the Grothendieck universe, Von Neumann universe.

The type of all types is called `Set`

in agda. Now, in constructing this type of all types naively we encounter a bunch of paradoxes, namely Russel’s Paradox, Cantor’s Paradox, Girard’s Paradox etc. These can be avoided by constructing the type of all types as “universes” in a heirarchically cumulative way. When we consider our universe to be the set of all types, we say that our universe is constructed heirarchically, with an index `i`

such that universe `Uᵢ`

∈ Uᵢ₊₁ and so on.

\[ U_{0} \in U_{1} \in U\_{2} \in ... \in U_{i} \in U_{i+1} \in ... \in U_{\infty} \]

Let us define the above index `i`

of universe `Uᵢ`

, called `Level`

in agda’s standard library:

We define it as a postulate so we dont have to provide an implementation yet. We continue to define some operations on it, i.e.:

`lzero`

, the trivial level 0`lsuc`

: successive iterator`_⊔_`

: least upper bound, an operator that composes

And finally, we define universe as:

```
record Universe u e : Set (lsuc (u ⊔ e)) where
field
-- Codes.
U : Set u
-- Decoding function.
El : U → Set e
```

A “family” of types varying over a given type are called, well “families of types”. An example of this would be the finite set, Fin where every finite set has `n`

elements where `n ∈ ℕ`

and hence `Fin`

, the creator of finite sets, is dependent on ℕ.

Mathematical sets cannot be directly represented in Agda as they are subject to Russel’s Paradox. However, sets are defined in a way similar to universes.

- Generally a set is represented by
`Set₁`

. - There exist infinite other
`Setᵢ`

such that`Set₁ : Set₂ : Set₃ : ...`

In fact, These `Setᵢ`

s are nothing but universes in Agda. Note that `Set₁`

forms the large set, i.e. the set containing all sets.

In some implementations, universes are represented using a different keyword `Type`

instead of `Set`

in order to avoid confusing with them:

```
Type : (i : AgdaLevel) → Set (alsuc i)
Type i = Set i
Type₀ = Type alzero
Type0 = Type alzero
Type₁ = Type (alsuc alzero)
Type1 = Type (alsuc alzero)
```

Now, given that we have infinite heirarchical universes, we would have to define the same functions, data types and machinery for each universe level, which would be pretty tedious to say the least. However, we observe how our universes are defined and note that the level-based indexing system, that connects each successive universe, provides us with the mechanics to define objects for all universe levels `ℓ`

:

Here `id`

represents a family of identity functions given a type `A`

and its level `ℓ`

.

```
infixr 5 _::_
data List₁ {ℓ : AgdaLevel} (A : Set ℓ) : Set (alsuc ℓ) where
[] : List₁ A
_::_ : A → List₁ A → List₁ A
someList : List₁ ℕ
someList = (one :: zero :: [])
sameList : List₁ ℕ
sameList = id someList
```

We obviously need a means to check types:

The equality of types is itself a type - the identity type: