\begin{code}
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}
\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₁(extensionality((λ 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}