Martin Escardo 2011.

\begin{code}

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

module DiscreteAndSeparated where

open import SetsAndFunctions
open import CurryHoward
open import Equality
open import DecidableAndDetachable
open import SumDisjoint

isolated : {X : Set} → (x : X) → Prp
isolated x = ∀ y → decidable(x ≡ y)

discrete : Set → Prp
discrete X = ∀(x : X) → isolated x

\end{code}

A simple example:

\begin{code}

open import Two

₂-discrete : discrete ₂
₂-discrete ₀ ₀ = in₀ refl
₂-discrete ₀ ₁ = in₁(λ ())
₂-discrete ₁ ₀ = in₁(λ ())
₂-discrete ₁ ₁ = in₀ refl

\end{code}

General properties:

\begin{code}

discrete-is-cotransitive : {X : Set} →

discrete X → ∀{x y z : X} → x ≢ y →  x ≢ z  ∨  z ≢ y

discrete-is-cotransitive d {x} {y} {z} φ = f(d x z)
where
f : x ≡ z  ∨  x ≢ z → x ≢ z  ∨  z ≢ y
f (in₀ r) = in₁ (λ s → φ(trans r s))
f (in₁ γ) = in₀ γ

separated : Set → Prp
separated X = ∀(x y : X) → ¬¬(x ≡ y) → x ≡ y

discrete-is-separated : {X : Set} →

discrete X → separated X

discrete-is-separated d x y = ¬¬-elim(d x y)

₂-separated : separated ₂
₂-separated = discrete-is-separated ₂-discrete

\end{code}

Separated sets form an exponential ideal, assuming
extensionality. More generally:

\begin{code}

separated-ideal : {X : Set} → {Y : X → Set} →

(∀ x → separated(Y x)) → separated((x : X) → Y x)

separated-ideal s f g h = funext lemma₂
where
open import Extensionality

lemma₀ : f ≡ g → ∀ x → f x ≡ g x
lemma₀ r x = cong (λ h → h x) r

lemma₁ : ∀ x → ¬¬(f x ≡ g x)
lemma₁ = DNU(¬¬-functor lemma₀ h)

lemma₂ : ∀ x → f x ≡ g x
lemma₂ x =  s x (f x) (g x) (lemma₁ x)

open import Injection

subtype-of-separated-is-separated : {X Y : Set} (m : X → Y) → left-cancellable m → separated Y → separated X
subtype-of-separated-is-separated {X} m i s x x' e = i (s (m x) (m x') (¬¬-functor (cong m) e))

\end{code}

The following is an apartness relation when Y is separated, but we
define it without this assumption. (Are all types separated? See
below.)

\begin{code}

infix 21 _♯_

_♯_ : {X : Set} → {Y : X → Set} → (f g : (x : X) → Y x) → Prp
f ♯ g = ∃ \x → f x ≢ g x

apart-is-different : {X : Set} → {Y : X → Set} →

∀{f g : (x : X) → Y x} → f ♯ g → f ≢ g

apart-is-different (x , φ) r = φ (cong (λ h → h x) r)

apart-is-symmetric : {X : Set} → {Y : X → Set} →

∀{f g : (x : X) → Y x} → f ♯ g → g ♯ f

apart-is-symmetric (x , φ)  = (∃-intro x (φ ∘ sym))

apart-is-cotransitive : {X : Set} → {Y : X → Set} →

(∀ x → discrete(Y x))
→ ∀(f g h : (x : X) → Y x) → f ♯ g → f ♯ h  ∨  h ♯ g

apart-is-cotransitive d f g h (x , φ)  = lemma₁(lemma₀ φ)
where
lemma₀ : f x ≢ g x → f x ≢ h x  ∨  h x ≢ g x
lemma₀ = discrete-is-cotransitive (d x)

lemma₁ : f x ≢ h x  ∨  h x ≢ g x → f ♯ h  ∨  h ♯ g
lemma₁ (in₀ γ) = in₀ (∃-intro x γ)
lemma₁ (in₁ δ) = in₁ (∃-intro x δ)

\end{code}

We now consider two cases which render the apartness relation ♯ tight,
assuming extensionality:

\begin{code}

tight : {X : Set} → {Y : X → Set} →

(∀ x → separated(Y x)) → ∀(f g : (x : X) → Y x) → ¬(f ♯ g) → f ≡ g

tight s f g h = funext lemma₁
where
open import Extensionality

lemma₀ : ∀ x → ¬¬(f x ≡ g x)
lemma₀ = not-exists-implies-forall-not h

lemma₁ : ∀ x → f x ≡ g x
lemma₁ x = (s x (f x) (g x)) (lemma₀ x)

tight' : {X : Set} → {Y : X → Set} →

(∀ x → discrete(Y x)) → ∀(f g : (x : X) → Y x) → ¬(f ♯ g) → f ≡ g

tight' d = tight (λ x → discrete-is-separated(d x))

\end{code}

What about sums? The special case they reduce to binary products is
easy:

\begin{code}

binary-product-separated : {X Y : Set} →

separated X → separated Y → separated(X × Y)

binary-product-separated s t (x , y) (x' , y') φ =
lemma(lemma₀ φ)(lemma₁ φ)
where
lemma₀ : ¬¬((x , y) ≡ (x' , y')) → x ≡ x'
lemma₀ = (s x x') ∘ ¬¬-functor(cong π₀)

lemma₁ : ¬¬((x , y) ≡ (x' , y')) → y ≡ y'
lemma₁ = (t y y') ∘ ¬¬-functor(cong π₁)

lemma : x ≡ x' → y ≡ y' → (x , y) ≡ (x' , y')
lemma = cong₂ (_,_)

\end{code}

This proof doesn't work for general dependent sums, because, among
other things, (cong π₁) doesn't make sense in that case.  A different
special case is also easy:

\begin{code}

binary-sum-separated : {X Y : Set} →

separated X → separated Y → separated(X + Y)

binary-sum-separated {X} {Y} s t (in₀ x) (in₀ x') = lemma
where
claim : in₀ x ≡ in₀ x' → x ≡ x'
claim = cong p
where p : X + Y → X
p(in₀ u) = u
p(in₁ v) = x

lemma : ¬¬(in₀ x ≡ in₀ x') → in₀ x ≡ in₀ x'
lemma = (cong in₀) ∘ (s x x') ∘ ¬¬-functor claim
binary-sum-separated s t (in₀ x) (in₁ y) =  λ φ → ⊥-elim(φ sum-disjoint )
binary-sum-separated s t (in₁ y) (in₀ x)  = λ φ → ⊥-elim(φ (sum-disjoint ∘ sym))
binary-sum-separated {X} {Y} s t (in₁ y) (in₁ y') = lemma
where
claim : in₁ y ≡ in₁ y' → y ≡ y'
claim = cong q
where q : X + Y → Y
q(in₀ u) = y
q(in₁ v) = v

lemma : ¬¬(in₁ y ≡ in₁ y') → in₁ y ≡ in₁ y'
lemma = (cong in₁) ∘ (t y y') ∘ ¬¬-functor claim

\end{code}

In this second case we implicitly used the fact that the set of
indices ₀ and ₁ is discrete. I will think about the general case
later.

\begin{code}

totally-separated : Set → Set
totally-separated X = {x y : X} → ((p : X → ₂) → p x ≡ p y) → x ≡ y

totally-separated-is-separated : (X : Set) → totally-separated X → separated X
totally-separated-is-separated X t x y φ  = t h
where
a : (p : X → ₂) → p x ≢ p y → ∅
a p = φ ∘ contra-positive(cong p)
h : (p : X → ₂) → p x ≡ p y
h p = ₂-separated (p x) (p y) (a p)

\end{code}

We must not forget:

\begin{code}

{--

ddd-sum : {X : Set} → {Y : X → Set} →

discrete X → (∀(x : X) → discrete(Y x)) → discrete(Σ \(x : X) → Y x)

ddd-sum {X} {Y} d e (x , y) (x' , y') = {!!}
where
lemma₀ : (x , y) ≡ (x' , y') → x ≡ x'
lemma₀ = cong π₀

lemma₁ : (r : (x ≡ x')) → subst r y ≡ y'
lemma₁ r = {!!}

--}

\end{code}