\begin{code}
{-# OPTIONS --without-K --exact-split --safe #-}
module Omniscience where
open import SpartanMLTT
open import Two
omniscient : U → U
omniscient X = (p : X → 𝟚) → (Σ \(x : X) → p x ≡ ₀) + ((x : X) → p x ≡ ₁)
open import Naturals
LPO : U
LPO = omniscient ℕ
\end{code}\begin{code}
open import DiscreteAndSeparated
open import DecidableAndDetachable
apart-or-equal : {X : U} → {Y : X → U} →
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 FunExt
claim : (x : X) → f x ≢ g x + f x ≡ g x
claim x = +-commutative(d x (f x) (g x))
lemma₀ : Σ \(p : X → 𝟚) → (x : X) → (p x ≡ ₀ → f x ≢ g x) × (p x ≡ ₁ → f x ≡ g x)
lemma₀ = indicator claim
p : X → 𝟚
p = pr₁ lemma₀
lemma₁ : (Σ \x → p x ≡ ₀) + ((x : X) → p x ≡ ₁)
lemma₁ = φ p
lemma₂ : (Σ \x → p x ≡ ₀) + ((x : X) → p x ≡ ₁) → f ♯ g + f ≡ g
lemma₂(inl(x , r)) = inl(x , (pr₁(pr₂ lemma₀ x) r))
lemma₂(inr h) =
inr(funext((λ x → pr₂(pr₂ lemma₀ x) (h x))))
omniscient-discrete-discrete : {X : U} → {Y : X → U} →
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(inl a) = inr(apart-is-different a)
h(inr r) = inl r
omniscient-discrete-discrete' : {X Y : U} → omniscient X → discrete Y → discrete(X → Y)
omniscient-discrete-discrete' {X} {Y} φ d =
omniscient-discrete-discrete {X} {λ x → Y} φ (λ x → d)
\end{code}