Impredicative universes

module foundation.impredicative-universes where

open import foundation-core.propositions
open import foundation-core.small-types
open import foundation-core.universe-levels

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)