Universe levels

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

Created on 2022-01-27.
Last modified on 2025-04-25.

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.

Recent changes

• 2025-04-25. Fredrik Bakke. chore: Fix some links (#1411).
• 2023-08-01. Fredrik Bakke. Small constructions from large ones in order theory (#680).
• 2023-06-10. Egbert Rijke and Fredrik Bakke. Cleaning up synthetic homotopy theory (#649).
• 2023-06-08. Fredrik Bakke. Remove empty foundation modules and replace them by their core counterparts (#644).
• 2023-06-07. Fredrik Bakke. Move public imports before “Imports” block (#642).