This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Universe levels

module foundation.universe-levels where

open import Agda.Primitive
  using (Level ; lzero ; lsuc ; _⊔_)
  renaming (Set to UU ; Setω to UUω)
  public

Idea

We import Agda's built in mechanism of universe levels. The universes are called UU, which stands for univalent universe, although we will not immediately assume that universes are univalent. This is done in foundation.univalence.