Martin Escardo 2011.

\begin{code}

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

module DiscreteAndSeparated where

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

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


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


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)

\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 = extensionality 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)

\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  _♯_

_♯_ : {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 = extensionality 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(φ lemma)
 where
  lemma : in₀ x ≡ in₁ y → ⊥
  lemma ()
binary-sum-separated s t (in₁ y) (in₀ x)  = λ φ → ⊥-elim(φ lemma)
 where
  lemma : in₁ y ≡ in₀ x → ⊥
  lemma ()
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.

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}