The principle of omniscience

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

Created on 2022-04-09.
Last modified on 2026-05-02.

module foundation.principle-of-omniscience where
Imports 
open import foundation.decidable-subtypes
open import foundation.dependent-products-propositions
open import foundation.propositional-truncations
open import foundation.universe-levels

open import foundation-core.decidable-propositions
open import foundation-core.propositions

Idea

A type X is said to satisfy the principle of omniscience if every decidable subtype of X is either inhabited or empty.

Definition

is-omniscient-Prop : {l : Level} → UU l → Prop (lsuc lzero ⊔ l)
is-omniscient-Prop X =
  Π-Prop
    ( decidable-subtype lzero X)
    ( λ P → is-decidable-Prop (trunc-Prop (type-decidable-subtype P)))

is-omniscient : {l : Level} → UU l → UU (lsuc lzero ⊔ l)
is-omniscient X = type-Prop (is-omniscient-Prop X)

See also

Recent changes