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-L̈of 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, 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
agree.

We give an example of a type X whose total separatedness implies WLPO
(Bishop's 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. 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. But assuming extensionality we get a
stronger result, which is not restricted to closed terms, and which is
a theorem rather than a metatheorem.

\begin{code}

{-# OPTIONS --without-K --exact-split --safe #-}

module FailureOfTotalSeparatedness where

open import SpartanMLTT
open import Two
open import Naturals
open import GenericConvergentSequence
open import BasicDiscontinuityTaboo
open import WLPO

open import Sets

\end{code}

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 and conceptual argument.)

\begin{code}

module concrete-example where

X : U
X = Σ \(u : ℕ∞) → u ≡ ∞ → 𝟚

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

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

\end{code}

The elements ∞₀ and ∞₁ look different:

\begin{code}

naive : (pr₂ ∞₀ refl ≡ ₀)  ×  (pr₂ ∞₁ refl ≡ ₁)
naive = refl , refl

\end{code}

But there is no function p : X → 𝟚 such that p x = pr₂ x refl, because
pr₁ x may be different from ∞, in which case pr₂ 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 = pr₂ x refl

doesn't type check (Agda says: "(pr₁ (pr₁ x) x) != ₁ of type 𝟚 when
checking that the expression refl has type pr₁ x ≡ ∞"), and hence we
haven't distinguished ∞₀ and ∞₁ by applying the same function to
them. This is clearly seen when enough implicit arguments are made
explicit.

No matter how hard we try to find such a function, we won't succeed,
because we know that WLPO is not provable:

\begin{code}

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

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

lemma : (n : ℕ) → p₀(under n) ≡ p₁(under n)
lemma n = ap (λ h → p(under n , h)) (funext claim)
where
open import FunExt
claim : (r : under n ≡ ∞) → (λ r → ₀) r ≡ (λ r → ₁) r
claim s = ∅-elim(∞-is-not-ℕ n (sym s))

\end{code}

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

\begin{code}

∞₀-and-∞₁-different : ∞₀ ≢ ∞₁
∞₀-and-∞₁-different r = zero-is-not-one claim₃
where
p : ∞ ≡ ∞
p = ap pr₁ r

φ : {x x' : ℕ∞} → x ≡ x' → (x ≡ ∞ → 𝟚) → (x' ≡ ∞ → 𝟚)
φ = transport _

claim₀ : φ p (λ p → ₀) ≡ (λ p → ₁)
claim₀ = Σ-≡-lemma ∞₀ ∞₁ r

claim₁ : φ p (λ p → ₀) refl ≡ ₁
claim₁ = ap (λ f → f refl) claim₀

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

claim₂ : ₀ ≡ φ p (λ p → ₀) refl
claim₂ = ap (λ p → φ p (λ p → ₀) refl) fact

claim₃ : ₀ ≡ ₁
claim₃ =  trans claim₂ claim₁

\end{code}

We can generalize this as follows, without using ℕ∞.

From an arbitrary given type X and distinguised element a : X, we
construct a new type Y, which will fail to be totally separated unless
the point a is weakly isolated. The idea is to "explode" the point a
into two different copies, which cannot be distinguished unless point
a is weakly isolated, and keep all the other original points
unchanged.

\begin{code}

module general-example (X : U) (a : X) where

Y : U
Y = Σ \(x : X) → x ≡ a → 𝟚

e : 𝟚 → X → Y
e n x = (x , λ p → n)

a₀ : Y
a₀ = e ₀ a

a₁ : Y
a₁ = e ₁ a

\end{code}

It is not easy to show that a₀ ≠ a₁. Here is our original proof using
the assumption that X is a set:

\begin{code}

Proposition : isSet X → a₀ ≢ a₁
Proposition h r = zero-is-not-one zero-is-one
where
p : a ≡ a
p = ap pr₁ r

φ : {x x' : X} → x ≡ x' → (x ≡ a → 𝟚) → (x' ≡ a → 𝟚)
φ = transport _

claim₀ : φ p (λ p → ₀) ≡ (λ p → ₁)
claim₀ = Σ-≡-lemma a₀ a₁ r

claim₁ : φ p (λ p → ₀) refl ≡ ₁
claim₁ = ap (λ f → f refl) claim₀

fact : refl ≡ p
fact = h refl p

claim₂ : ₀ ≡ φ p (λ p → ₀) refl
claim₂ = ap (λ p → φ p (λ p → ₀) refl) fact

zero-is-one : ₀ ≡ ₁
zero-is-one =  trans claim₂ claim₁

\end{code}

Eventually we found a proof that doesn't require the assumption that X
is a set. The idea is to use U, rather than 𝟚, to distinguish points
(of course!):

\begin{code}

Proposition' : a₀ ≢ a₁
Proposition' r = zero-is-not-one zero-is-one
where
P : Y → U
P (x , f) = Σ \(q : x ≡ a) → f q ≡ ₁

observation₀ : P a₀ ≡ (a ≡ a × ₀ ≡ ₁)
observation₀ = refl

observation₁ : P a₁ ≡ (a ≡ a × ₁ ≡ ₁)
observation₁ = refl

f : P a₁ → P a₀
f = transport P (sym r)

p₁ : P a₁
p₁ = refl , refl

p₀ : P a₀
p₀ = f p₁

zero-is-one : ₀ ≡ ₁
zero-is-one = pr₂ p₀

\end{code}

Points different from the point a are mapped to the same point by the
two embeddings e₀ and e₁:

\begin{code}

Lemma : (x : X) → x ≢ a → e ₀ x ≡ e ₁ x
Lemma x φ = ap (λ ψ → (x , ψ)) claim
where
open import FunExt
claim : (λ p → ₀) ≡ (λ p → ₁)
claim = funext(λ p → ∅-elim(φ p))

\end{code}

The following theorem shows that, because not every type X has
decidable equality, the points a₀,a₁ of Y cannot necessarily be
distinguished by maps into the discrete set 𝟚. To get the desired
conclusion, it is enough to consider X = (ℕ → 𝟚), which is separated,
in the sense that ¬¬(x ≡ y) → x ≡ y, assuming extensionality. (Cf. the
module DiscreteAndSeparated.lagda.)

\begin{code}

open import DecidableAndDetachable

weakly-isolated : {X : U} (x : X) → U
weakly-isolated x = ∀ x' → decidable(x' ≢ x)

Theorem : (Σ \(g : Y → 𝟚) → g a₀ ≢ g a₁) → weakly-isolated a
Theorem (g , d) = λ x → two-equality-cases' (claim₀' x) (claim₁' x)
where
f : X → 𝟚
f x = g(e ₀ x) ⊕ g(e ₁ x)

claim₀ : f a ≡ ₁
claim₀ = Lemma[b≢c→b⊕c≡₁] d

claim₁ : (x : X) → x ≢ a → f x ≡ ₀
claim₁ x φ = Lemma[b≡c→b⊕c≡₀] (ap g (Lemma x φ))

claim₀' : (x : X) → f x ≡ ₀ → x ≢ a
claim₀' x p r = ∅-elim (Lemma[b≡₀→b≢₁] fact claim₀)
where
fact : f a ≡ ₀
fact = trans (ap f (sym r)) p

claim₁' : (x : X) → f x ≡ ₁ → ¬(x ≢ a)
claim₁' x p φ = ∅-elim(Lemma[b≡₀→b≢₁] fact p)
where
fact : f x ≡ ₀
fact = claim₁ x φ

\end{code}