Impredicative universes

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

Created on 2022-06-02.
Last modified on 2024-04-11.

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 𝒰 is impredicative if the type of propositions in 𝒰 is 𝒰-small.

Definition

is-impredicative-UU : (l : Level) → UU (lsuc l)
is-impredicative-UU l = is-small l (Prop l)

See also

Recent changes