Martin Escardo 2011.

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

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

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
UF.Miscelanea (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 Ξ³

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

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

\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-is-h-isolated : {X : 𝓀 Μ‡ } (x : X) β†’ is-isolated x β†’ is-h-isolated x
isolated-is-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-is-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-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 𝓀 π“₯
                                                         β†’ (Ξ£ yβ‚€ κž‰ Y , Ξ£ y₁ κž‰ Y , yβ‚€ β‰  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-is-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}