This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

The principle of omniscience

module foundation.principle-of-omniscience where
Imports 
open import foundation.decidable-subtypes
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