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}