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}