Martin Escardo 2011.


{-# 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 = omniscient 


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:


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₁
  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)
  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)