Martin Escardo 2011. \begin{code} {-# OPTIONS --without-K #-} module Omniscience where open import SetsAndFunctions open import CurryHoward open import Equality open import Two omniscient : Set → Prp omniscient X = ∀(p : X → ₂) → (∃ \(x : X) → p x ≡ ₀) ∨ (∀(x : X) → p x ≡ ₁) open import Naturals LPO : Prp LPO = omniscient ℕ \end{code} Notice that LPO is Bishop's limited principle of omniscience, which is a taboo, in Aczel's terminology. The negation of LPO is false, but LPO is not provable, and hence LPO is independent. In classical mathematics it is uncomfortable to have independent propositions, but of course unavoidable. Independence occurs often in constructive mathematics, particular in classically compatible constructive mathematics, like Bishop's methamatics and Martin-Löf type theory (in its various flavours); even the principle of excluded middle is independent: it cannot be proved, but its negation is false. We'll see that the infinite set ℕ∞ defined in the module ConvergentSequence is omniscient. If a set X is omniscient and a set Y has is has decidable equality, then the function space (X → Y) has decidable equality, if we assume extensionality. In our topological correspondence, decidable equality is called discreteness. More generally we have: \begin{code} open import DiscreteAndSeparated open import DecidableAndDetachable apart-or-equal : {X : Set} → {Y : X → Set} → omniscient X → (∀(x : X) → discrete(Y x)) → ∀(f g : (x : X) → Y x) → f ♯ g ∨ f ≡ g apart-or-equal {X} {Y} φ d f g = lemma₂ lemma₁ where open import Extensionality claim : ∀ x → f x ≢ g x ∨ f x ≡ g x claim x = ∨-commutative(d x (f x) (g x)) lemma₀ : ∃ \p → ∀ x → (p x ≡ ₀ → f x ≢ g x) ∧ (p x ≡ ₁ → f x ≡ g x) lemma₀ = indicator claim p : X → ₂ p = ∃-witness lemma₀ lemma₁ : (∃ \x → p x ≡ ₀) ∨ (∀(x : X) → p x ≡ ₁) lemma₁ = φ p lemma₂ : (∃ \x → p x ≡ ₀) ∨ (∀(x : X) → p x ≡ ₁) → f ♯ g ∨ f ≡ g lemma₂(in₀(x , r)) = in₀(∃-intro x(∧-elim₀(∃-elim lemma₀ x) r)) lemma₂(in₁ h) = in₁(funext((λ x → ∧-elim₁(∃-elim lemma₀ x) (h x)))) omniscient-discrete-discrete : {X : Set} → {Y : X → Set} → omniscient X → (∀(x : X) → discrete(Y x)) → discrete((x : X) → Y x) omniscient-discrete-discrete {X} {Y} φ d f g = h(apart-or-equal φ d f g) where h : f ♯ g ∨ f ≡ g → f ≡ g ∨ f ≢ g h(in₀ a) = in₁(apart-is-different a) h(in₁ r) = in₀ r omniscient-discrete-discrete' : {X Y : Set} → omniscient X → discrete Y → discrete(X → Y) omniscient-discrete-discrete' {X} {Y} φ d = omniscient-discrete-discrete {X} {λ x → Y} φ (λ x → d) \end{code}