Martin Escardo 2011.

(Totally separated types moved to the module TotallySeparated January
2018, and extended.)

\begin{code}

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

module DiscreteAndSeparated where

open import SpartanMLTT

open import Two-Properties
open import Plus-Properties
open import NaturalNumbers-Properties
open import DecidableAndDetachable
open import UF-Base
open import UF-Subsingletons renaming (⊤Ω to  ; ⊥Ω to )
open import UF-Subsingletons-FunExt
open import UF-Equiv
open import UF-Retracts
open import UF-FunExt

is-isolated : {X : 𝓤 ̇ }  X  𝓤 ̇
is-isolated x =  y  decidable (x  y)

is-perfect : 𝓤 ̇  𝓤 ̇
is-perfect X = is-empty (Σ x  X , is-isolated x)

is-isolated' : {X : 𝓤 ̇ }  X  𝓤 ̇
is-isolated' x =  y  decidable (y  x)

decidable-eq-sym : {X : 𝓤 ̇ } (x y : X)  decidable (x  y)  decidable (y  x)
decidable-eq-sym x y = cases
                         (p : x  y)  inl (p ⁻¹))
                         (n : ¬ (x  y))  inr  (q : y  x)  n (q ⁻¹)))

-is-isolated'-gives-is-isolated : {X : 𝓤 ̇ } (x : X)  is-isolated' x  is-isolated x
-is-isolated'-gives-is-isolated x i' y = cases
                                    (p : y  x)  inl (p ⁻¹))
                                    (n : ¬ (y  x))  inr  (p : x  y)  n (p ⁻¹)))
                                   (i' y)

is-isolated'-gives-is-isolated : {X : 𝓤 ̇ } (x : X)  is-isolated' x  is-isolated x
is-isolated'-gives-is-isolated x i' y = decidable-eq-sym y x (i' y)

is-isolated-gives-is-isolated' : {X : 𝓤 ̇ } (x : X)  is-isolated x  is-isolated' x
is-isolated-gives-is-isolated' x i y = decidable-eq-sym x y (i y)

is-discrete : 𝓤 ̇  𝓤 ̇
is-discrete X = (x : X)  is-isolated x

\end{code}

Standard examples:

\begin{code}

props-are-discrete : {P : 𝓤 ̇ }  is-prop P  is-discrete P
props-are-discrete i x y = inl (i x y)

𝟘-is-discrete : is-discrete (𝟘 {𝓤})
𝟘-is-discrete = props-are-discrete 𝟘-is-prop

𝟙-is-discrete : is-discrete (𝟙 {𝓤})
𝟙-is-discrete = props-are-discrete 𝟙-is-prop

𝟚-is-discrete : is-discrete 𝟚
𝟚-is-discrete   = inl refl
𝟚-is-discrete   = inr  (p :   )  𝟘-elim (zero-is-not-one p))
𝟚-is-discrete   = inr  (p :   )  𝟘-elim (zero-is-not-one (p ⁻¹)))
𝟚-is-discrete   = inl refl

ℕ-is-discrete : is-discrete 
ℕ-is-discrete 0 0 = inl refl
ℕ-is-discrete 0 (succ n) = inr  (p : zero  succ n)  positive-not-zero n (p ⁻¹))
ℕ-is-discrete (succ m) 0 = inr  (p : succ m  zero)  positive-not-zero m p)
ℕ-is-discrete (succ m) (succ n) =  step (ℕ-is-discrete m n)
  where
   step : (m  n) + (m  n)  (succ m  succ n) + (succ m  succ n)
   step (inl r) = inl (ap succ r)
   step (inr f) = inr  s  f (succ-lc s))

+-is-discrete : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
           is-discrete X  is-discrete Y  is-discrete (X + Y)
+-is-discrete d e (inl x) (inl x') =
    Cases (d x x')
      (p : x  x')  inl (ap inl p))
      (n : ¬ (x  x'))  inr (contrapositive inl-lc n))
+-is-discrete d e (inl x) (inr y) = inr +disjoint
+-is-discrete d e (inr y) (inl x) = inr +disjoint'
+-is-discrete d e (inr y) (inr y') =
    Cases (e y y')
      (p : y  y')  inl (ap inr p))
      (n : ¬ (y  y'))  inr (contrapositive inr-lc n))

\end{code}

The closure of discrete types under Σ is proved in the module
UF-Miscelanea (as this requires to first prove that discrete types
are sets).

General properties:

\begin{code}

discrete-is-cotransitive : {X : 𝓤 ̇ }
                          is-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  φ (r  s))
  f (inr γ) = inl γ

retract-is-discrete : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
                     retract Y of X  is-discrete X  is-discrete Y
retract-is-discrete (f , (s , φ)) d y y' = g (d (s y) (s y'))
 where
  g : decidable (s y  s y')  decidable (y  y')
  g (inl p) = inl ((φ y) ⁻¹  ap f p  φ y')
  g (inr u) = inr (contrapositive (ap s) u)

𝟚-retract-of-non-trivial-type-with-isolated-point : {X : 𝓤 ̇ } {x₀ x₁ : X}  x₀  x₁
                                                   is-isolated x₀  retract 𝟚 of X
𝟚-retract-of-non-trivial-type-with-isolated-point {𝓤} {X} {x₀} {x₁} ne d = r , (s , rs)
 where
  r : X  𝟚
  r = pr₁ (characteristic-function d)
  φ : (x : X)  (r x    x₀  x) × (r x    ¬ (x₀  x))
  φ = pr₂ (characteristic-function d)
  s : 𝟚  X
  s  = x₀
  s  = x₁
  rs : (n : 𝟚)  r (s n)  n
  rs  = different-from-₁-equal-₀  p  pr₂ (φ x₀) p refl)
  rs  = different-from-₀-equal-₁ λ p  𝟘-elim (ne (pr₁ (φ x₁) p))

𝟚-retract-of-discrete : {X : 𝓤 ̇ } {x₀ x₁ : X}  x₀  x₁  is-discrete X  retract 𝟚 of X
𝟚-retract-of-discrete {𝓤} {X} {x₀} {x₁} ne d = 𝟚-retract-of-non-trivial-type-with-isolated-point ne (d x₀)

\end{code}

¬¬-Separated types form an exponential ideal, assuming
extensionality. More generally:

\begin{code}

is-¬¬-separated : 𝓤 ̇  𝓤 ̇
is-¬¬-separated X = (x y : X)  ¬¬-stable (x  y)

Π-is-¬¬-separated : funext 𝓤 𝓥
                   {X : 𝓤 ̇ } {Y : X  𝓥 ̇ }
                   ((x : X)  is-¬¬-separated (Y x))
                   is-¬¬-separated (Π Y)
Π-is-¬¬-separated fe s f g h = dfunext fe lemma₂
 where
  lemma₀ : f  g   x  f x  g x
  lemma₀ r x = ap  -  - x) r
  lemma₁ :  x  ¬¬ (f x  g x)
  lemma₁ = double-negation-unshift (¬¬-functor lemma₀ h)
  lemma₂ :  x  f x  g x
  lemma₂ x =  s x (f x) (g x) (lemma₁ x)

discrete-is-¬¬-separated : {X : 𝓤 ̇ }  is-discrete X  is-¬¬-separated X
discrete-is-¬¬-separated d x y = ¬¬-elim (d x y)

𝟚-is-¬¬-separated : is-¬¬-separated 𝟚
𝟚-is-¬¬-separated = discrete-is-¬¬-separated 𝟚-is-discrete

subtype-is-¬¬-separated : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (m : X  Y)
                                      left-cancellable m
                                      is-¬¬-separated Y
                                      is-¬¬-separated X
subtype-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 : 𝓤 ̇ }  {Y : X  𝓥 ̇ }  (f g : (x : X)  Y x)  𝓤  𝓥 ̇
f  g = Σ x  domain f , f x  g x


apart-is-different : {X : 𝓤 ̇ } {Y : X  𝓥 ̇ }
                    {f g : (x : X)  Y x}  f  g  f  g
apart-is-different (x , φ) r = φ (ap  -  - x) r)


apart-is-symmetric : {X : 𝓤 ̇ }  {Y : X  𝓥 ̇ }
                    {f g : (x : X)  Y x}  f  g  g  f
apart-is-symmetric (x , φ)  = (x , (φ  _⁻¹))

apart-is-cotransitive : {X : 𝓤 ̇ }  {Y : X  𝓥 ̇ }
                      ((x : X)  is-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 : 𝓤 ̇ }
       funext 𝓤 𝓥
       {Y : X  𝓥 ̇ }
       ((x : X)  is-¬¬-separated (Y x))
       (f g : (x : X)  Y x)
       ¬ (f  g)  f  g
tight fe s f g h = dfunext fe lemma₁
 where
  lemma₀ :  x  ¬¬ (f x  g x)
  lemma₀ = not-Σ-implies-Π-not h
  lemma₁ :  x  f x  g x
  lemma₁ x = (s x (f x) (g x)) (lemma₀ x)

tight' : {X : 𝓤 ̇ }
        funext 𝓤 𝓥
        {Y : X  𝓥 ̇ }
        ((x : X)  is-discrete (Y x))  (f g : (x : X)  Y x)  ¬ (f  g)  f  g
tight' fe d = tight fe  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-is-¬¬-separated : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
                                is-¬¬-separated X
                                is-¬¬-separated Y
                                is-¬¬-separated (X × Y)
binary-product-is-¬¬-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 pr₁) doesn't make sense in that case.  A different
special case is also easy:

\begin{code}

binary-sum-is-¬¬-separated : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
                            is-¬¬-separated X
                            is-¬¬-separated Y
                            is-¬¬-separated (X + Y)
binary-sum-is-¬¬-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-is-¬¬-separated s t (inl x) (inr y) =  λ φ  𝟘-elim (φ +disjoint )
binary-sum-is-¬¬-separated s t (inr y) (inl x)  = λ φ  𝟘-elim (φ (+disjoint  _⁻¹))
binary-sum-is-¬¬-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

⊥-⊤-density' : funext 𝓤 𝓤
              propext 𝓤
               {𝓥} {X : 𝓥 ̇ }
              is-¬¬-separated X
              (f : Ω 𝓤  X)  f   f 
              wconstant f
⊥-⊤-density' fe pe s f r p q = g p  (g q)⁻¹
  where
    a :  p  ¬¬ (f p  f )
    a p t = no-truth-values-other-than-⊥-or-⊤ fe pe (p , (b , c))
      where
        b : p  
        b u = t (ap f u  r)

        c : p  
        c u = t (ap f u)

    g :  p  f p  f 
    g p = s (f p) (f ) (a p)

\end{code}

Added 19th March 2021.

\begin{code}

equality-of-¬¬stable-propositions' : propext 𝓤
                                    (P Q : 𝓤 ̇ )
                                    is-prop P
                                    is-prop Q
                                    ¬¬-stable P
                                    ¬¬-stable Q
                                    ¬¬-stable (P  Q)
equality-of-¬¬stable-propositions' pe P Q i j f g a = V
 where
  I : ¬¬ (P  Q)
  I = ¬¬-functor (transport id) a

  II : P  Q
  II = →-is-¬¬-stable g I

  III : ¬¬ (Q  P)
  III = ¬¬-functor (transport id  _⁻¹) a

  IV : Q  P
  IV = →-is-¬¬-stable f III

  V : P  Q
  V = pe i j II IV

equality-of-¬¬stable-propositions : funext 𝓤 𝓤
                                   propext 𝓤
                                   (p q : Ω 𝓤)
                                   ¬¬-stable (p holds)
                                   ¬¬-stable (q holds)
                                   ¬¬-stable (p  q)
equality-of-¬¬stable-propositions fe pe p q f g a = γ
 where
  δ : p holds  q holds
  δ = equality-of-¬¬stable-propositions'
       pe (p holds) (q holds) (holds-is-prop p) (holds-is-prop q)
       f g (¬¬-functor (ap _holds) a)

  γ : p  q
  γ = to-subtype-≡  _  being-prop-is-prop fe) δ


Ω¬¬ : (𝓤 : Universe)   𝓤  ̇
Ω¬¬ 𝓤 = Σ p  Ω 𝓤 , ¬¬-stable (p holds)

Ω¬¬-is-¬¬-separated : funext 𝓤 𝓤
                     propext 𝓤
                     is-¬¬-separated (Ω¬¬ 𝓤)
Ω¬¬-is-¬¬-separated fe pe (p , s) (q , t) ν = γ
 where
  α : ¬¬ (p  q)
  α = ¬¬-functor (ap pr₁) ν

  δ : p  q
  δ = equality-of-¬¬stable-propositions fe pe p q s t α

  γ : (p , s)  (q , t)
  γ = to-subtype-≡  p  Π-is-prop fe  _  holds-is-prop p)) δ

⊥-⊤-Density : funext 𝓤 𝓤
             propext 𝓤
             {X : 𝓥 ̇ }
              (f : Ω 𝓤  X)
             is-¬¬-separated X
             f   f 
             (p : Ω 𝓤)  f p  f 
⊥-⊤-Density fe pe f s r p = s (f p) (f ) a
 where
  a : ¬¬ (f p  f )
  a u = no-truth-values-other-than-⊥-or-⊤ fe pe (p , b , c)
   where
    b : p  
    b v = u (ap f v  r)

    c : p  
    c w = u (ap f w)

⊥-⊤-density : funext 𝓤 𝓤
             propext 𝓤
             (f : Ω 𝓤  𝟚)
             f   
             f   
             (p : Ω 𝓤)  f p  
⊥-⊤-density fe pe f r s p = ⊥-⊤-Density fe pe f 𝟚-is-¬¬-separated (r  s ⁻¹) p  s

\end{code}

21 March 2018

\begin{code}

qinvs-preserve-isolatedness : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X  Y)  qinv f
                             (x : X)  is-isolated x  is-isolated (f x)
qinvs-preserve-isolatedness {𝓤} {𝓥} {X} {Y} f (g , ε , η) x i y = h (i (g y))
 where
  h : decidable (x  g y)  decidable (f x  y)
  h (inl p) = inl (ap f p  η y)
  h (inr u) = inr (contrapositive  (q : f x  y)  (ε x)⁻¹  ap g q) u)

equivs-preserve-isolatedness : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X  Y)  is-equiv f
                              (x : X)  is-isolated x  is-isolated (f x)
equivs-preserve-isolatedness f e = qinvs-preserve-isolatedness f (equivs-are-qinvs f e)

new-point-is-isolated : {X : 𝓤 ̇ }  is-isolated {𝓤  𝓥} {X + 𝟙 {𝓥}} (inr *)
new-point-is-isolated {𝓤} {𝓥} {X} = h
 where
  h :  (y : X + 𝟙)  decidable (inr *  y)
  h (inl x) = inr +disjoint'
  h (inr *) = inl refl

\end{code}

Back to old stuff:

\begin{code}

≡-indicator :  (m : )  Σ p  (  𝟚) , ((n : )  (p n    m  n) × (p n    m  n))
≡-indicator m = co-characteristic-function (ℕ-is-discrete m)

χ≡ :     𝟚
χ≡ m = pr₁ (≡-indicator m)

χ≡-spec : (m n : )  (χ≡ m n    m  n) × (χ≡ m n    m  n)
χ≡-spec m = pr₂ (≡-indicator m)

_≡[ℕ]_ :     𝓤₀ ̇
m ≡[ℕ] n = (χ≡ m n)  

infix  30 _≡[ℕ]_

≡-agrees-with-≡[ℕ] : (m n : )  m  n  m ≡[ℕ] n
≡-agrees-with-≡[ℕ] m n =  r  different-from-₀-equal-₁  s  pr₁ (χ≡-spec m n) s r)) , pr₂ (χ≡-spec m n)

≢-indicator :  (m : )  Σ p  (  𝟚) , ((n : )  (p n    m  n) × (p n    m  n))
≢-indicator m = indicator (ℕ-is-discrete m)

χ≢ :     𝟚
χ≢ m = pr₁ (≢-indicator m)

χ≢-spec : (m n : )  (χ≢ m n    m  n) × (χ≢ m n    m  n)
χ≢-spec m = pr₂ (≢-indicator m)

_≠_ :     𝓤₀ ̇
m  n = (χ≢ m n)  

infix  30 _≠_

≠-agrees-with-≢ : (m n : )  m  n  m  n
≠-agrees-with-≢ m n = pr₂ (χ≢-spec m n) ,  d  different-from-₀-equal-₁ (contrapositive (pr₁ (χ≢-spec m n)) d))

\end{code}

Added 14th Feb 2020:

\begin{code}

discrete-exponential-has-decidable-emptiness-of-exponent : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
                                                          funext 𝓤 𝓥
                                                          (Σ y₀  Y , Σ y₁  Y , y₀  y₁)
                                                          is-discrete (X  Y)
                                                          decidable (is-empty X)
discrete-exponential-has-decidable-emptiness-of-exponent {𝓤} {𝓥} {X} {Y} fe (y₀ , y₁ , ne) d = γ
 where
  a : decidable ((λ _  y₀)   _  y₁))
  a = d  _  y₀)  _  y₁)

  f : decidable ((λ _  y₀)   _  y₁))  decidable (is-empty X)
  f (inl p) = inl g
   where
    g : is-empty X
    g x = ne q
     where
      q : y₀  y₁
      q = ap  -  - x) p

  f (inr ν) = inr (contrapositive g ν)
   where
    g : is-empty X   _  y₀)   _  y₁)
    g ν = dfunext fe  x  𝟘-elim (ν x))

  γ : decidable (is-empty X)
  γ = f a

\end{code}