This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.
Impredicative universes
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)