Universe levels

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2022-01-27.
Last modified on 2023-08-01.

module foundation.universe-levels where

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


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.

Recent changes