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