Small universes

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

Created on 2022-03-03.
Last modified on 2023-06-08.

module foundation.small-universes where

open import foundation.universe-levels

open import foundation-core.cartesian-product-types
open import foundation-core.small-types

Idea

A universe UU l1 is said to be small with respect to UU l2 if UU l1 is a UU l2-small type and each X : UU l1 is a UU l2-small type

is-small-universe :
  (l l1 : Level) → UU (lsuc l1 ⊔ lsuc l)
is-small-universe l l1 = is-small l (UU l1) × ((X : UU l1) → is-small l X)

Recent changes

• 2023-06-08. Fredrik Bakke. Remove empty foundation modules and replace them by their core counterparts (#644).
• 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).
• 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
• 2023-03-07. Fredrik Bakke. Add blank lines between <details> tags and markdown syntax (#490).
• 2023-03-07. Jonathan Prieto-Cubides. Show module declarations (#488).