Martin Escardo 2011.


{-# 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


A simple example:


open import Two

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


General properties:


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)
  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


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


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

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

separated-ideal s f g h = funext lemma₂
  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))


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


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₀ φ)
  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 δ)


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


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₁
  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))


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


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₁ φ)
  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₂ (_,_)


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:


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
  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
  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


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


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
  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)


We must not forget:



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') = {!!}
   lemma₀ : (x , y) ≡ (x' , y') → x ≡ x'
   lemma₀ = cong π₀

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