Impredicative universes
Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.
Created on 2022-06-02.
Last modified on 2023-06-08.
module foundation.impredicative-universes where
Imports
open import foundation.universe-levels open import foundation-core.propositions open import foundation-core.small-types
Idea
A universe U
is impredicative if the type of propositions in U
is U
-small.
Definition
is-impredicative-UU : (l : Level) → UU (lsuc l) is-impredicative-UU l = is-small l (Prop l)
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-07. Fredrik Bakke. Add blank lines between
<details>
tags and markdown syntax (#490). - 2023-03-07. Jonathan Prieto-Cubides. Show module declarations (#488).
- 2023-03-06. Fredrik Bakke. Remove redundant whitespace in headers (#486).