Martin Escardo 2011.

\begin{code}

{-# OPTIONS --without-K --exact-split --safe #-}

module DiscreteAndSeparated where

open import SpartanMLTT
open import DecidableAndDetachable
open import SumDisjoint

isolated : {X : U}  (x : X)  U
isolated x =  y  decidable(x  y)


discrete : U  U
discrete X = (x : X)  isolated x

\end{code}

A simple example:

\begin{code}

open import Two

𝟚-discrete : discrete 𝟚
𝟚-discrete   = inl refl
𝟚-discrete   = inr ())
𝟚-discrete   = inr ())
𝟚-discrete   = inl refl

\end{code}

General properties:

\begin{code}

discrete-is-cotransitive : {X : U}  

 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 (inl r) = inr  s  φ(trans r s)) 
  f (inr γ) = inl γ 


separated : U  U
separated X = (x y : X)  ¬¬(x  y)  x  y


discrete-is-separated : {X : U} 

 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 : U}  {Y : X  U}  

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

separated-ideal s f g h = funext lemma𝟚
 where 
  open import FunExt

  lemma₀ : f  g   x  f x  g x
  lemma₀ r x = ap  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 : U} (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 (ap 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 : U}  {Y : X  U}  (f g : (x : X)  Y x)  U
f  g = Σ \x  f x  g x


apart-is-different : {X : U} {Y : X  U}  

 {f g : (x : X)  Y x}  f  g  f  g

apart-is-different (x , φ) r = φ (ap  h  h x) r)


apart-is-symmetric : {X : U}  {Y : X  U}  

 {f g : (x : X)  Y x}  f  g  g  f

apart-is-symmetric (x , φ)  = (x , (φ  sym)) 


apart-is-cotransitive : {X : U}  {Y : X  U}  

 ((x : 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₁ (inl γ) = inl (x , γ)
  lemma₁ (inr δ) = inr (x , δ)

\end{code}

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

\begin{code}

tight : {X : U}  {Y : X  U}  

 ((x : X)  separated(Y x))  (f g : (x : X)  Y x)  ¬(f  g)  f  g

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

  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 : U}  {Y : X  U}  

 ((x : 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 : U}  

  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(ap pr₁)

  lemma₁ : ¬¬((x , y)  (x' , y'))  y  y'
  lemma₁ = (t y y')  ¬¬-functor(ap pr₂)

  lemma : x  x'  y  y'  (x , y)  (x' , y')
  lemma = ap₂ (_,_)  

\end{code}

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

\begin{code}

binary-sum-separated : {X Y : U}  

  separated X  separated Y  separated(X + Y)

binary-sum-separated {X} {Y} s t (inl x) (inl x') = lemma 
 where
  claim : inl x  inl x'  x  x'
  claim = ap p
   where p : X + Y  X
         p(inl u) = u
         p(inr v) = x

  lemma : ¬¬(inl x  inl x')  inl x  inl x'
  lemma = (ap inl)  (s x x')  ¬¬-functor claim
binary-sum-separated s t (inl x) (inr y) =  λ φ  ∅-elim(φ sum-disjoint )  
binary-sum-separated s t (inr y) (inl x)  = λ φ  ∅-elim(φ(sum-disjoint  sym)) 
binary-sum-separated {X} {Y} s t (inr y) (inr y') = lemma 
 where
  claim : inr y  inr y'  y  y'
  claim = ap q
   where q : X + Y  Y
         q(inl u) = y
         q(inr v) = v

  lemma : ¬¬(inr y  inr y')  inr y  inr y'
  lemma = (ap inr)  (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 : U  U
totally-separated X = {x y : X}  ((p : X  𝟚)  p x  p y)  x  y

totally-separated-is-separated : (X : U)  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(ap 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 : U} → {Y : X → U} → 

  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₀ = ap π₀

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

--}

\end{code}