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
Imports
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).