Martin Escardo, Jan 2013.

Alternative to FailureOfTotalSeparatedness.lagda

The point is that we don't need fancy types such as ℕ∞, and we don't
need to refer to continuity. We only need to know that certain types
cannot provably have decidable equality (meta-theorem). Also we make
UIP into an assumption (we start with an hset). But we still need to
assume function extensionality.

(We are still fond of the example given in the above file, which is
anyway very similar.)

\begin{code}

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

module FailureOfTotalSeparatednessBis where

open import HSets
open import Two
open import SetsAndFunctions
open import Equality
open import Extensionality
open import CurryHoward

module assumptions (X : Set) (h : hset X) (a : X) where

\end{code}

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

\begin{code}

Y : Set
Y = Σ \(x : X) → x ≡ a → ₂

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

a₀ : Y
a₀ = e a ₀

a₁ : Y
a₁ = e a ₁

\end{code}

It is not easy to show that a₀ ≠ a₁.  We use the assumption that X is
an hset. (But surely this must be the case even if X is not assumed to
be an hset?)

\begin{code}

Proposition : a₀ ≢ a₁
Proposition r = zero-is-not-one claim₃
where
p : a ≡ a
p = cong π₀ r

claim₀ : subst {X} {λ x → x ≡ a → ₂} p (λ p → ₀) ≡ (λ p → ₁)
claim₀ = Σ-≡-lemma a₀ a₁ r

claim₁ : subst {X} {λ r → r ≡ a → ₂} p (λ p → ₀) refl ≡ ₁
claim₁ = cong (λ f → f refl) claim₀

fact : refl ≡ p
fact = h refl p

claim₂ : ₀ ≡ subst {X} {λ r → r ≡ a → ₂} p (λ p → ₀) refl
claim₂ = cong (λ p → subst {X} {λ r → r ≡ a → ₂} p (λ p → ₀) refl) fact

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

Lemma : ∀(x : X) → x ≢ a → e x ₀ ≡ e x ₁
Lemma x φ = cong (λ ψ → (x , ψ)) claim
where
claim : (λ p → ₀) ≡ (λ p → ₁)
claim = funext(λ p → ⊥-elim(φ p))

\end{code}

The following theorem shows that, because not every type X has
decidable equality, the elements 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 : Set} (x : X) → Set
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≡₀] (cong 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 (cong 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}