Martin Escardo, 20 Feb 2012.

We give a negative answer to a question posed by Altenkirch, Anberrée
and Li.

They asked whether for every definable type X in Martin-Lof type
theory, it is the case that for any two provably distinct elements 
x₀, x₁ : X, there is a function p: X→₂ and a proof 
d: p x₀ ≠ p x₁. Here ₂ is the type of binary numerals, or booleans if
you like, but I am not telling you which of ₀ and ₁ is to be regarded
as true or false.

If one thinks of ₂-valued maps as characteristic functions of clopen
sets in a topological view of types, then their question amounts to
asking whether the definable types are totally separated, that is,
whether the clopens separate the points. See Johnstone's book "Stone
Spaces" for some information about this notion - e.g. for compact
spaces, it agrees with total disconnectedness (the connected
components are the singletons) and zero-dimensionality (the clopens
form a base of the topology), but in general the three notions don't

We give an example of a type X whose total separatedness implies WLPO
(the weak limited principle of omniscience). The proof works by
constructing two elements x₀ and x₁ of X, and a discontinuous function
ℕ∞→₂ from any hypothetical p:X→₂ with p x₀ ≠ p x₁, and then reducing
discontinuity to WLPO.

Our proof postulates extensionality, which entitles us to use UIP on
the type ℕ∞. Without the postulate there are fewer closed terms of
type X→₂, and their question was for closed terms X, x₀,x₁:X, and
d:x₀≠x₁, and so the negative answer also works in the absence of
extensionality and of UIP for ℕ∞. But assuming extensionality we get a
stronger result, which is not restricted to closed terms. 


{-# OPTIONS --without-K #-}

module FailureOfTotalSeparatedness where

open import Two
open import GenericConvergentSequence
open import SetsAndFunctions
open import Equality
open import BasicDiscontinuityTaboo
open import WLPO
open import Extensionality
open import CurryHoward
open import HSets


The idea of the following construction is that we replace ∞ in ℕ∞ by
two copies ∞₀ and ∞₁, which are different but not distinguishable by
maps into ₂, unless WLPO holds. (We can use the Cantor space (ℕ→₂) or
the Baire space (ℕ → ℕ), or many other types instead of ℕ∞, with ∞
replaced by any fixed element. But I think the proposed construction
gives a more transparent argument.)


X : Set
X = Σ \(u : ℕ∞)  u    

∞₀ : X
∞₀ = ( , λ r  )

∞₁ : X
∞₁ = ( , λ r  )


The elements ∞₀ and ∞₁ look different:


naive : π₁ ∞₀ refl      π₁ ∞₁ refl  
naive = ∧-intro refl refl


But there is no function p : X → ₂ such that p x = π₁ x refl, because
π₀ x may be different from ∞, in which case π₁ x is the function with
empty graph, and so it can't be applied to anything, and certainly not
to refl. In fact, the definition 

    p : X → ₂
    p x = π₁ x refl 

doesn't type check, and hence we haven't distinguished ∞₀ and ∞₁ by
applying the same function to them. This is clearly seen when the
implicit arguments are made explicit.

No matter how hard we try to find such a function, we won't succeed:


failure : ∀(p : X  )  p ∞₀  p ∞₁  WLPO
failure p = disagreement-taboo p₀ p₁ lemma
  p₀ : ℕ∞  
  p₀ u = p(u , λ r  ) 

  p₁ : ℕ∞  
  p₁ u = p(u , λ r  ) 

  lemma :  n  p₀(under n)  p₁(under n)
  lemma n = cong  h  p(under n , h)) (funext claim)
    claim : ∀(r : under n  )   r  ) r   r  ) r
    claim s = ⊥-elim(∞-is-not-ℕ n (sym s))


Precisely because one cannot construct maps from X into ₂ that
distinguish ∞₀ and ∞₁, it is a bit tricky to prove that they are
indeed different:


∞₀-and-∞₁-different : ∞₀  ∞₁
∞₀-and-∞₁-different r = zero-is-not-one claim₃
  p :   
  p = cong π₀ r

  claim₀ : subst {ℕ∞}  u  u    } p  p  )   p  )
  claim₀ = Σ-≡-lemma ∞₀ ∞₁ r

  claim₁ : subst {ℕ∞}  r  r    } p  p  ) refl  
  claim₁ = cong  f  f refl) claim₀

  fact : refl  p
  fact = ℕ∞-hset refl p

  claim₂ :   subst {ℕ∞}  r  r    } p  p  ) refl
  claim₂ = cong  p  subst {ℕ∞}  r  r    } p  p  ) refl) fact

  claim₃ :   
  claim₃ =  trans claim₂ claim₁