Martin Escardo 2011.

\begin{code}

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

module UF.DiscreteAndSeparated where

open import MLTT.Spartan

open import MLTT.Plus-Properties
open import MLTT.Two-Properties
open import Naturals.Properties
open import NotionsOfDecidability.Complemented
open import NotionsOfDecidability.Decidable
open import UF.Base
open import UF.Embeddings
open import UF.Equiv
open import UF.FunExt
open import UF.Hedberg
open import UF.HedbergApplications
open import UF.PropTrunc
open import UF.Retracts
open import UF.Sets
open import UF.SubtypeClassifier
open import UF.Subsingletons
open import UF.Subsingletons-FunExt

is-isolated : {X : ๐“ค ฬ‡ } โ†’ X โ†’ ๐“ค ฬ‡
is-isolated x = โˆ€ y โ†’ is-decidable (x ๏ผ y)

\end{code}

Notice that there is a different notion of being homotopy isolated
(abbreviated is-h-isolated) in the module UF.Sets. We show below that
isolated points are h-isolated.

A type is perfect if it has no isolated points.

\begin{code}

is-perfect : ๐“ค ฬ‡ โ†’ ๐“ค ฬ‡
is-perfect X = is-empty (ฮฃ x ๊ž‰ X , is-isolated x)

is-isolated' : {X : ๐“ค ฬ‡ } โ†’ X โ†’ ๐“ค ฬ‡
is-isolated' x = โˆ€ y โ†’ is-decidable (y ๏ผ x)

is-decidable-eq-sym : {X : ๐“ค ฬ‡ } (x y : X)
                    โ†’ is-decidable (x ๏ผ y)
                    โ†’ is-decidable (y ๏ผ x)
is-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 = is-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 = is-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))

inl-is-isolated : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (x : X)
                โ†’ is-isolated x
                โ†’ is-isolated (inl x)
inl-is-isolated {๐“ค} {๐“ฅ} {X} {Y} x i = ฮณ
 where
  ฮณ : (z : X + Y) โ†’ is-decidable (inl x ๏ผ z)
  ฮณ (inl x') = Cases (i x')
                (ฮป (p : x ๏ผ x') โ†’ inl (ap inl p))
                (ฮป (n : ยฌ (x ๏ผ x')) โ†’ inr (contrapositive inl-lc n))
  ฮณ (inr y)  = inr +disjoint

inr-is-isolated : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (y : Y)
                โ†’ is-isolated y
                โ†’ is-isolated (inr y)
inr-is-isolated {๐“ค} {๐“ฅ} {X} {Y} y i = ฮณ
 where
  ฮณ : (z : X + Y) โ†’ is-decidable (inr y ๏ผ z)
  ฮณ (inl x)  = inr +disjoint'
  ฮณ (inr y') = Cases (i y')
                (ฮป (p : y ๏ผ y') โ†’ inl (ap inr p))
                (ฮป (n : ยฌ (y ๏ผ y')) โ†’ inr (contrapositive inr-lc n))

+-is-discrete : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ }
              โ†’ is-discrete X
              โ†’ is-discrete Y
              โ†’ is-discrete (X + Y)
+-is-discrete d e (inl x) = inl-is-isolated x (d x)
+-is-discrete d e (inr y) = inr-is-isolated y (e y)

\end{code}

The closure of discrete types under ฮฃ is proved in the module
TypeTopology.SigmaDiscreteAndTotallySeparated (as this requires to
first prove that discrete types are sets).

General properties:

\begin{code}

discrete-types-are-cotransitive : {X : ๐“ค ฬ‡ }
                                 โ†’ is-discrete X
                                 โ†’ {x y z : X}
                                 โ†’ x โ‰  y
                                 โ†’ (x โ‰  z) + (z โ‰  y)
discrete-types-are-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 ฮณ

discrete-types-are-cotransitive' : {X : ๐“ค ฬ‡ }
                                 โ†’ is-discrete X
                                 โ†’ {x y z : X}
                                 โ†’ x โ‰  y
                                 โ†’ (x โ‰  z) + (y โ‰  z)
discrete-types-are-cotransitive' d {x} {y} {z} ฯ† = f (d x z)
 where
  f : (x ๏ผ z) + (x โ‰  z) โ†’ (x โ‰  z) + (y โ‰  z)
  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 : is-decidable (s y ๏ผ s y') โ†’ is-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

โ„•-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))

Cantor-is-ยฌยฌ-separated : funextโ‚€ โ†’ is-ยฌยฌ-separated (โ„• โ†’ ๐Ÿš)
Cantor-is-ยฌยฌ-separated fe = ฮ -is-ยฌยฌ-separated fe (ฮป _ โ†’ ๐Ÿš-is-ยฌยฌ-separated)

\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-types-are-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 function 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) ฮด

โŠฅ-โŠค-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 : is-decidable (x ๏ผ g y) โ†’ is-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 + ๐Ÿ™) โ†’ is-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}

We now show that discrete types are sets (Hedberg's Theorem).

\begin{code}

decidable-types-are-collapsible : {X : ๐“ค ฬ‡ } โ†’ is-decidable X โ†’ collapsible X
decidable-types-are-collapsible (inl x) = pointed-types-are-collapsible x
decidable-types-are-collapsible (inr u) = empty-types-are-collapsible u

discrete-is-Id-collapsible : {X : ๐“ค ฬ‡ } โ†’ is-discrete X โ†’ Id-collapsible X
discrete-is-Id-collapsible d = decidable-types-are-collapsible (d _ _)

discrete-types-are-sets : {X : ๐“ค ฬ‡ } โ†’ is-discrete X โ†’ is-set X
discrete-types-are-sets d =
 Id-collapsibles-are-sets (discrete-is-Id-collapsible d)

being-isolated-is-prop : FunExt โ†’ {X : ๐“ค ฬ‡ } (x : X) โ†’ is-prop (is-isolated x)
being-isolated-is-prop {๐“ค} fe x = prop-criterion ฮณ
 where
  ฮณ : is-isolated x โ†’ is-prop (is-isolated x)
  ฮณ i = ฮ -is-prop (fe ๐“ค ๐“ค)
         (ฮป x โ†’ sum-of-contradictory-props
                 (local-hedberg _
                   (ฮป y โ†’ decidable-types-are-collapsible (i y)) x)
                 (negations-are-props (fe ๐“ค ๐“คโ‚€))
                 (ฮป p n โ†’ n p))

being-isolated'-is-prop : FunExt โ†’ {X : ๐“ค ฬ‡ } (x : X) โ†’ is-prop (is-isolated' x)
being-isolated'-is-prop {๐“ค} fe x = prop-criterion ฮณ
 where
  ฮณ : is-isolated' x โ†’ is-prop (is-isolated' x)
  ฮณ i = ฮ -is-prop (fe ๐“ค ๐“ค)
         (ฮป x โ†’ sum-of-contradictory-props
                 (local-hedberg' _
                   (ฮป y โ†’ decidable-types-are-collapsible (i y)) x)
                 (negations-are-props (fe ๐“ค ๐“คโ‚€))
                 (ฮป p n โ†’ n p))

being-discrete-is-prop : FunExt โ†’ {X : ๐“ค ฬ‡ } โ†’ is-prop (is-discrete X)
being-discrete-is-prop {๐“ค} fe = ฮ -is-prop (fe ๐“ค ๐“ค) (being-isolated-is-prop fe)

isolated-points-are-h-isolated : {X : ๐“ค ฬ‡ } (x : X)
                               โ†’ is-isolated x
                               โ†’ is-h-isolated x
isolated-points-are-h-isolated {๐“ค} {X} x i {y} = local-hedberg x (ฮป y โ†’ ฮณ y (i y)) y
 where
  ฮณ : (y : X) โ†’ is-decidable (x ๏ผ y) โ†’ ฮฃ f ๊ž‰ (x ๏ผ y โ†’ x ๏ผ y) , wconstant f
  ฮณ y (inl p) = (ฮป _ โ†’ p) , (ฮป q r โ†’ refl)
  ฮณ y (inr n) = id , (ฮป q r โ†’ ๐Ÿ˜-elim (n r))

isolated-inl : {X : ๐“ค ฬ‡ } (x : X) (i : is-isolated x) (y : X) (r : x ๏ผ y)
             โ†’ i y ๏ผ inl r
isolated-inl x i y r =
  equality-cases (i y)
   (ฮป (p : x ๏ผ y) (q : i y ๏ผ inl p)
      โ†’ q โˆ™ ap inl (isolated-points-are-h-isolated x i p r))
   (ฮป (h : x โ‰  y) (q : i y ๏ผ inr h)
      โ†’ ๐Ÿ˜-elim(h r))

isolated-inr : {X : ๐“ค ฬ‡ }
             โ†’ funext ๐“ค ๐“คโ‚€
             โ†’ (x : X) (i : is-isolated x) (y : X) (n : x โ‰  y) โ†’ i y ๏ผ inr n
isolated-inr fe x i y n =
  equality-cases (i y)
   (ฮป (p : x ๏ผ y) (q : i y ๏ผ inl p)
      โ†’ ๐Ÿ˜-elim (n p))
   (ฮป (m : x โ‰  y) (q : i y ๏ผ inr m)
      โ†’ q โˆ™ ap inr (dfunext fe (ฮป (p : x ๏ผ y) โ†’ ๐Ÿ˜-elim (m p))))

\end{code}

The following variation of the above doesn't require function extensionality:

\begin{code}

isolated-inr' : {X : ๐“ค ฬ‡ }
                (x : X)
                (i : is-isolated x)
                (y : X)
                (n : x โ‰  y)
              โ†’ ฮฃ m ๊ž‰ x โ‰  y , i y ๏ผ inr m
isolated-inr' x i y n =
  equality-cases (i y)
   (ฮป (p : x ๏ผ y) (q : i y ๏ผ inl p)
      โ†’ ๐Ÿ˜-elim (n p))
   (ฮป (m : x โ‰  y) (q : i y ๏ผ inr m)
      โ†’ m , q)

discrete-inl : {X : ๐“ค ฬ‡ }
               (d : is-discrete X)
               (x y : X)
               (r : x ๏ผ y)
             โ†’ d x y ๏ผ inl r
discrete-inl d x = isolated-inl x (d x)

discrete-inl-refl : {X : ๐“ค ฬ‡ }
                    (d : is-discrete X)
                    (x : X)
                  โ†’ d x x ๏ผ inl refl
discrete-inl-refl {๐“ค} {X} d x = discrete-inl d x x refl

discrete-inr : funext ๐“ค ๐“คโ‚€
             โ†’ {X : ๐“ค ฬ‡ }
               (d : is-discrete X)
               (x y : X)
               (n : ยฌ (x ๏ผ y))
             โ†’ d x y ๏ผ inr n
discrete-inr fe d x = isolated-inr fe x (d x)

isolated-Id-is-prop : {X : ๐“ค ฬ‡ } (x : X)
                    โ†’ is-isolated' x
                    โ†’ (y : X) โ†’ is-prop (y ๏ผ x)
isolated-Id-is-prop x i =
 local-hedberg' x (ฮป y โ†’ decidable-types-are-collapsible (i y))

lc-maps-reflect-isolatedness : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y)
                             โ†’ left-cancellable f
                             โ†’ (x : X) โ†’ is-isolated (f x) โ†’ is-isolated x
lc-maps-reflect-isolatedness f l x i y = ฮณ (i (f y))
 where
  ฮณ : (f x ๏ผ f y) + ยฌ (f x ๏ผ f y) โ†’ (x ๏ผ y) + ยฌ (x ๏ผ y)
  ฮณ (inl p) = inl (l p)
  ฮณ (inr n) = inr (contrapositive (ap f) n)

lc-maps-reflect-discreteness : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y)
                             โ†’ left-cancellable f
                             โ†’ is-discrete Y
                             โ†’ is-discrete X
lc-maps-reflect-discreteness f l d x =
 lc-maps-reflect-isolatedness f l x (d (f x))

embeddings-reflect-isolatedness : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y)
                                โ†’ is-embedding f
                                โ†’ (x : X) โ†’ is-isolated (f x)
                                โ†’ is-isolated x
embeddings-reflect-isolatedness f e x i y = lc-maps-reflect-isolatedness f
                                              (embeddings-are-lc f e) x i y

equivs-reflect-isolatedness : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y)
                            โ†’ is-equiv f
                            โ†’ (x : X) โ†’ is-isolated (f x)
                            โ†’ is-isolated x
equivs-reflect-isolatedness f e = embeddings-reflect-isolatedness f
                                   (equivs-are-embeddings f e)

embeddings-reflect-discreteness : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y)
                                โ†’ is-embedding f
                                โ†’ is-discrete Y
                                โ†’ is-discrete X
embeddings-reflect-discreteness f e = lc-maps-reflect-discreteness f (embeddings-are-lc f e)

equivs-preserve-discreteness : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (f : X โ†’ Y)
                             โ†’ is-equiv f
                             โ†’ is-discrete X
                             โ†’ is-discrete Y
equivs-preserve-discreteness f e = lc-maps-reflect-discreteness
                                     (inverse f e)
                                     (equivs-are-lc
                                        (inverse f e)
                                        (inverses-are-equivs f e))

equiv-to-discrete : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ }
                  โ†’ X โ‰ƒ Y
                  โ†’ is-discrete X
                  โ†’ is-discrete Y
equiv-to-discrete (f , e) = equivs-preserve-discreteness f e

๐Ÿ™-is-set : is-set (๐Ÿ™ {๐“ค})
๐Ÿ™-is-set = discrete-types-are-sets ๐Ÿ™-is-discrete

๐Ÿš-is-set : is-set ๐Ÿš
๐Ÿš-is-set = discrete-types-are-sets ๐Ÿš-is-discrete

โ„•-is-set : is-set โ„•
โ„•-is-set = discrete-types-are-sets โ„•-is-discrete

\end{code}

Added 14th Feb 2020:

\begin{code}

discrete-exponential-has-decidable-emptiness-of-exponent
 : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ }
 โ†’ funext ๐“ค ๐“ฅ
 โ†’ has-two-distinct-points Y
 โ†’ is-discrete (X โ†’ Y)
 โ†’ is-decidable (is-empty X)
discrete-exponential-has-decidable-emptiness-of-exponent
  {๐“ค} {๐“ฅ} {X} {Y} fe ((yโ‚€ , yโ‚) , ne) d = ฮณ
 where
  a : is-decidable ((ฮป _ โ†’ yโ‚€) ๏ผ (ฮป _ โ†’ yโ‚))
  a = d (ฮป _ โ†’ yโ‚€) (ฮป _ โ†’ yโ‚)

  f : is-decidable ((ฮป _ โ†’ yโ‚€) ๏ผ (ฮป _ โ†’ yโ‚)) โ†’ is-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))

  ฮณ : is-decidable (is-empty X)
  ฮณ = f a

\end{code}

Added 19th Feb 2020:

\begin{code}

maps-of-props-into-h-isolated-points-are-embeddings
 : {P : ๐“ค ฬ‡ } {X : ๐“ฅ ฬ‡ } (f : P โ†’ X)
 โ†’ is-prop P
 โ†’ ((p : P) โ†’ is-h-isolated (f p))
 โ†’ is-embedding f
maps-of-props-into-h-isolated-points-are-embeddings f i j q (p , s) (p' , s') =
 to-ฮฃ-๏ผ (i p p' , j p' _ s')

maps-of-props-into-isolated-points-are-embeddings : {P : ๐“ค ฬ‡ } {X : ๐“ฅ ฬ‡ }
                                                    (f : P โ†’ X)
                                                  โ†’ is-prop P
                                                  โ†’ ((p : P) โ†’ is-isolated (f p))
                                                  โ†’ is-embedding f
maps-of-props-into-isolated-points-are-embeddings f i j =
 maps-of-props-into-h-isolated-points-are-embeddings f i
  (ฮป p โ†’ isolated-points-are-h-isolated (f p) (j p))

global-point-is-embedding : {X : ๐“ค ฬ‡ } (f : ๐Ÿ™ {๐“ฅ} โ†’ X)
                          โ†’ is-h-isolated (f โ‹†)
                          โ†’ is-embedding f
global-point-is-embedding f h =
 maps-of-props-into-h-isolated-points-are-embeddings
  f ๐Ÿ™-is-prop h'
   where
    h' : (p : ๐Ÿ™) โ†’ is-h-isolated (f p)
    h' โ‹† = h

\end{code}

Added 1st May 2024. Wrapper for use with instance arguments:

\begin{code}

record is-discrete' {๐“ค : Universe} (X : ๐“ค ฬ‡ ) : ๐“ค ฬ‡ where
 constructor
  discrete-gives-discrete'
 field
  discrete'-gives-discrete : is-discrete X

open is-discrete' {{...}} public

\end{code}

Added 14th October 2024. We move the notion of weakly isolated point
from its original place FailureOfTotalSeparatedness (added there some
time in 2013 for a paper with Thomas Streicher on the indiscreteness
of the universe and related things). Then we add further properties of
this notion, used both in the module FailureOfTotalSeparatedness and
the module Ordinals.NotationInterpretation.

\begin{code}

is-weakly-isolated : {X : ๐“ค ฬ‡ } (x : X) โ†’ ๐“ค ฬ‡
is-weakly-isolated x = โˆ€ x' โ†’ is-decidable (x' โ‰  x)

isolated-gives-weakly-isolated : {X : ๐“ค ฬ‡ } (x : X)
                               โ†’ is-isolated x
                               โ†’ is-weakly-isolated x
isolated-gives-weakly-isolated x i y =
 Cases (i y)
  (ฮป (e : x ๏ผ y) โ†’ inr (ฮป (d : y โ‰  x) โ†’ d (e โปยน)))
  (ฮป (d : x โ‰  y) โ†’ inl (ฮป (e : y ๏ผ x) โ†’ d (e โปยน)))

equivs-preserve-weak-isolatedness : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ }
                                    (f : X โ‰ƒ Y)
                                  โ†’ (x : X)
                                  โ†’ is-weakly-isolated x
                                  โ†’ is-weakly-isolated (โŒœ f โŒ x)
equivs-preserve-weak-isolatedness f x i y =
 Cases (i (โŒœ f โŒโปยน y))
  (ฮป (a : โŒœ f โŒโปยน y โ‰  x)
     โ†’ inl (ฮป (e : y ๏ผ โŒœ f โŒ x)
            โ†’ a (โŒœ f โŒโปยน y         ๏ผโŸจ ap โŒœ f โŒโปยน e โŸฉ
                 โŒœ f โŒโปยน (โŒœ f โŒ x) ๏ผโŸจ inverses-are-retractions' f x โŸฉ
                 x                 โˆŽ)))
  (ฮป (b : ยฌ (โŒœ f โŒโปยน y โ‰  x))
     โ†’ inr (ฮป (d : y โ‰  โŒœ f โŒ x)
            โ†’ b (ฮป (e : โŒœ f โŒโปยน y ๏ผ x)
                 โ†’ d (y                 ๏ผโŸจ (inverses-are-sections' f y)โปยน โŸฉ
                      โŒœ f โŒ (โŒœ f โŒโปยน y) ๏ผโŸจ ap โŒœ f โŒ e โŸฉ
                      โŒœ f โŒ x           โˆŽ))))

equivs-reflect-weak-isolatedness : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ }
                                 โ†’ (f : X โ‰ƒ Y)
                                 โ†’ (x : X) โ†’ is-weakly-isolated (โŒœ f โŒ x)
                                 โ†’ is-weakly-isolated x
equivs-reflect-weak-isolatedness f x i = II
 where
  I : is-weakly-isolated (โŒœ f โŒโปยน (โŒœ f โŒ x))
  I = equivs-preserve-weak-isolatedness (โ‰ƒ-sym f) (โŒœ f โŒ x) i

  II : is-weakly-isolated x
  II = transport is-weakly-isolated (inverses-are-retractions' f x) I

\end{code}

TODO (in another module). More generally, if an equivalence preserve
some property, it also reflects it.