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 Two-Prop-Density
open import UF-Base
open import UF-Subsingletons
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-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}

𝟘-is-discrete : is-discrete (𝟘 {𝓀})
𝟘-is-discrete ()

πŸ™-is-discrete : is-discrete (πŸ™ {𝓀})
πŸ™-is-discrete * * = inl refl

𝟚-is-discrete : is-discrete 𝟚
𝟚-is-discrete β‚€ β‚€ = inl refl
𝟚-is-discrete β‚€ ₁ = inr(Ξ» ())
𝟚-is-discrete ₁ β‚€ = inr(Ξ» ())
𝟚-is-discrete ₁ ₁ = inl refl

β„•-is-discrete : is-discrete β„•
β„•-is-discrete 0 0 = inl refl
β„•-is-discrete 0 (succ n) = inr (Ξ»())
β„•-is-discrete (succ m) 0 = inr (Ξ»())
β„•-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))

+discrete : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
          β†’ is-discrete X β†’ is-discrete Y β†’ is-discrete (X + Y)
+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))
+discrete d e (inl x) (inr y) = inr +disjoint
+discrete d e (inr y) (inl x) = inr +disjoint'
+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-SetExamples (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-discrete-discrete : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                         β†’ retract Y of X β†’ is-discrete X β†’ is-discrete Y
retract-discrete-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-discrete : {X : 𝓀 Μ‡ } {xβ‚€ x₁ : X} β†’ xβ‚€ β‰’ x₁ β†’ is-discrete X β†’ retract 𝟚 of X
𝟚-retract-of-discrete {𝓀} {X} {xβ‚€} {x₁} ne d = r , (s , rs)
 where
  r : X β†’ 𝟚
  r = pr₁ (characteristic-function (d xβ‚€))
  Ο† : (x : X) β†’ (r x ≑ β‚€ β†’ xβ‚€ ≑ x) Γ— (r x ≑ ₁ β†’ Β¬ (xβ‚€ ≑ x))
  Ο† = prβ‚‚ (characteristic-function (d xβ‚€))
  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))

\end{code}

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

\begin{code}

is-separated : 𝓀 Μ‡ β†’ 𝓀 Μ‡
is-separated X = (x y : X) β†’ ¬¬(x ≑ y) β†’ 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-of-separated-is-separated : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (m : X β†’ Y)
                                  β†’ left-cancellable m β†’ is-separated Y β†’ is-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 : 𝓀 Μ‡ } β†’ {Y : X β†’ π“₯ Μ‡ } β†’ (f g : (x : X) β†’ Y x) β†’ 𝓀 βŠ” π“₯ Μ‡
f β™― g = Ξ£ \x β†’ 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 ⊀ β†’ constant 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}

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)

equivalences-preserve-isolatedness : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y) β†’ is-equiv f
                                   β†’ (x : X) β†’ is-isolated x β†’ is-isolated (f x)
equivalences-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 (Ξ» ())
  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}