Martin Escardo, 24th March 2022, with additions June 2024 and October 2026.

This file is a apropos the discussion at the end of the file
Ordinals.InductiveRecursiveCodesInterpretations.

\begin{code}

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

open import UF.FunExt

module Taboos.P2 (fe : Fun-Ext) where

private
 fe' : FunExt
 fe' 𝓀 π“₯ = fe {𝓀} {π“₯}

open import MLTT.Spartan
open import MLTT.Two-Properties
open import UF.Base
open import UF.ClassicalLogic
open import UF.DiscreteAndSeparated
open import UF.Equiv
open import UF.Equiv-FunExt
open import UF.Retracts
open import UF.Subsingletons
open import UF.Subsingletons-FunExt

\end{code}

The following map plays a central role in the investigations of this
file.

\begin{code}

Οƒ : (X : 𝓀 Μ‡ ) β†’ 𝟚 β†’ (X β†’ 𝟚)
Οƒ X n = Ξ» _ β†’ n

\end{code}

Abbreviations.

\begin{code}

Οƒβ‚€ : {X : 𝓀 Μ‡ } β†’ (X β†’ 𝟚)
Οƒβ‚€ {𝓀} {X} = Οƒ X β‚€

σ₁ : {X : 𝓀 Μ‡ } β†’ (X β†’ 𝟚)
σ₁ {𝓀} {X} = Οƒ X ₁

\end{code}

Recall that we say that a type X is empty to mean Β¬ X, namely X β†’ 𝟘,
and nonempty to mean ¬¬ X.

In general, if the type X is a proposition we will write "Β¬ X" rather
than the synonym "is-empty X", and "¬¬ X" rather than the synonym
"is-nonempty X". Also, we will pronounce "¬¬ X" as "X is irrefutable"
when X is a proposition.

\begin{code}

emptiness-criterion : (X : 𝓀 Μ‡ ) β†’ is-empty X ↔ (Οƒβ‚€ ＝ σ₁)
emptiness-criterion {𝓀} X = (f , g)
 where
  f : Β¬ X β†’ Οƒβ‚€ ＝ σ₁
  f Ξ½ = dfunext fe (Ξ» (x : X) β†’ 𝟘-elim (Ξ½ x))

  g : Οƒβ‚€ ＝ σ₁ β†’ Β¬ X
  g e x = zero-is-not-one
           (β‚€    ＝⟨refl⟩
            Οƒβ‚€ x ＝⟨ happly e x ⟩
            σ₁ x ＝⟨refl⟩
            ₁    ∎)

nonemptiness-criterion : (X : 𝓀 Μ‡ ) β†’ is-nonempty X ↔ (Οƒβ‚€ β‰  σ₁)
nonemptiness-criterion {𝓀} X = I (emptiness-criterion X)
 where
  I : type-of (emptiness-criterion X) β†’ ¬¬ X ↔ (Οƒβ‚€ β‰  σ₁)
  I (f , g) = (Ξ» (Ξ½ : ¬¬ X) (e : Οƒβ‚€ ＝ σ₁) β†’ Ξ½ (g e)) ,
              contrapositive f

\end{code}

The main notion studied in this file is the following:

\begin{code}

is-thinly-inhabited : 𝓀 Μ‡ β†’ 𝓀 Μ‡
is-thinly-inhabited X = is-equiv (Οƒ X)

being-thinly-inhabited-is-prop : {X : 𝓀 Μ‡ } β†’ is-prop (is-thinly-inhabited X)
being-thinly-inhabited-is-prop {𝓀} {X} = being-equiv-is-prop fe' (Οƒ X)

\end{code}

The idea of the terminology "thinly" is that there are very few
elements in the type, but at the same time the type is nonempty. As we
shall see, this is actually a notion stronger than nonemptiness. But
this idea works only for types that have enough functions into the
booleans, called totally separated. We show below that if X is totally
separated and thinly inhabited then X is a proposition.

Exercise. A type X is thinly inhabited if and only if there is *any*
equivalence 𝟚 ≃ (X β†’ 𝟚).

For propositions X, the thin inhabitedness of X is equivalent to the
map Οƒ X having a retraction ρ.

                            Οƒ X
                          𝟚  β†ͺ  (X β†’ 𝟚)
                          𝟚  β†ž  (X β†’ 𝟚)
                             ρ

In general there can be many maps ρ with ρ ∘ Οƒ X ∼ id, but there is at
most one if X is a proposition. We use the following lemma to prove
this:

\begin{code}

retraction-of-Οƒ-is-section : {P : 𝓀 Μ‡ }
                           β†’ is-prop P
                           β†’ (ρ : (P β†’ 𝟚) β†’ 𝟚)
                           β†’ ρ ∘ Οƒ P ∼ id
                           β†’ Οƒ P ∘ ρ ∼ id
retraction-of-Οƒ-is-section {𝓀} {P} i ρ h f = IV
 where
  I : (p : P) β†’ ρ f ＝ f p
  I p = ρ f           ＝⟨ ap ρ III ⟩
        ρ (Οƒ P (f p)) ＝⟨ h (f p) ⟩
        f p           ∎
   where
    II : f ∼ Οƒ P (f p)
    II q = f q         ＝⟨ ap f (i q p) ⟩
           f p         ＝⟨refl⟩
           Οƒ P (f p) q ∎

    III : f ＝ Οƒ P (f p)
    III = dfunext fe II

  IV : Οƒ P (ρ f) ＝ f
  IV = dfunext fe I

Οƒ-having-retraction-is-prop : {X : 𝓀 Μ‡ }
                            β†’ is-prop X
                            β†’ is-prop (has-retraction (Οƒ X))
Οƒ-having-retraction-is-prop {𝓀} {X} i =
 prop-criterion
  (Ξ» (ρ , ρσ) β†’ sections-have-at-most-one-retraction fe' (Οƒ X)
                 (ρ , retraction-of-Οƒ-is-section i ρ ρσ))

retraction-of-Οƒ-gives-thinly-inhabited : {P : 𝓀 Μ‡ }
                                       β†’ is-prop P
                                       β†’ has-retraction (Οƒ P)
                                       β†’ is-thinly-inhabited P
retraction-of-Οƒ-gives-thinly-inhabited {𝓀} {P} i (ρ , ρσ) =
 qinvs-are-equivs (Οƒ P) (ρ , ρσ , retraction-of-Οƒ-is-section i ρ ρσ)

\end{code}

For the converse we don't need X to be a proposition, of course.

\begin{code}

thinly-inhabited-gives-retraction-of-Οƒ : {X : 𝓀 Μ‡ }
                                       β†’ is-thinly-inhabited X
                                       β†’ has-retraction (Οƒ X)
thinly-inhabited-gives-retraction-of-Οƒ {𝓀} {X} = equivs-are-sections (Οƒ X)

\end{code}

By construction, every 𝟚-valued function on a thinly inhabited type is
constant.

\begin{code}

constancy : {X : 𝓀 Μ‡ }
          β†’ is-thinly-inhabited X
          β†’ (f : X β†’ 𝟚)
          β†’ Ξ£ n κž‰ 𝟚 , f ＝ Ξ» _ β†’ n
constancy {𝓀} {X} ti f = ⌜ e ⌝⁻¹ f , ((inverses-are-sections' e f)⁻¹)
 where
  e : 𝟚 ≃ (X β†’ 𝟚)
  e = Οƒ X , ti

\end{code}

Next we want to show that

 P β†’ is-thinly-inhabited P

for any proposition P, and we use the following lemma.

\begin{code}

point-gives-retraction-of-Οƒ : {X : 𝓀 Μ‡ }
                            β†’ X
                            β†’ has-retraction (Οƒ X)
point-gives-retraction-of-Οƒ {𝓀} {X} x = (Ξ³ , Ξ³Οƒ)
 where
  Ξ³ : (X β†’ 𝟚) β†’ 𝟚
  Ξ³ f = f x

  Ξ³Οƒ : Ξ³ ∘ Οƒ X ∼ id
  Ξ³Οƒ n = refl

point-gives-is-thinly-inhabited : {P : 𝓀 Μ‡ }
                                β†’ is-prop P
                                β†’ P
                                β†’ is-thinly-inhabited P
point-gives-is-thinly-inhabited {𝓀} {P} i p =
 retraction-of-Οƒ-gives-thinly-inhabited i (point-gives-retraction-of-Οƒ p)

\end{code}

Notice, however, that pointed types X other than propositions are not
thinly inhabited in general. An example is the type X := 𝟚, because there
are four maps X β†’ 𝟚 in this case, and we need exactly two to have an
equivalence.

We will see later that the following implication can't be reversed,
even for just propositions, unless weak excluded middle holds, so that
the notion of being thinly inhabited is stronger, in general, than
that of being nonempty.

\begin{code}

thinly-inhabited-gives-nonempty : {X : 𝓀 Μ‡ }
                                β†’ is-thinly-inhabited X
                                β†’ is-nonempty X
thinly-inhabited-gives-nonempty {𝓀} {X} ti Ξ½ = III
 where
  e : 𝟚 ≃ (X β†’ 𝟚)
  e = Οƒ X , ti

  I : ⌜ e ⌝⁻¹ Οƒβ‚€ ＝ ⌜ e ⌝⁻¹ σ₁
  I = ap (⌜ e ⌝⁻¹) (Οƒβ‚€ ＝⟨ dfunext fe (Ξ» x β†’ 𝟘-elim (Ξ½ x)) ⟩
                    σ₁ ∎)

  II = β‚€          ＝⟨ (inverses-are-retractions' e β‚€)⁻¹ ⟩
       ⌜ e ⌝⁻¹ Οƒβ‚€ ＝⟨ I ⟩
       ⌜ e ⌝⁻¹ σ₁ ＝⟨ inverses-are-retractions' e ₁ ⟩
       ₁          ∎

  III : 𝟘
  III = zero-is-not-one II

\end{code}

In some cases the implication

 P β†’ is-thinly-inhabited P

can be reversed:

\begin{code}

thinly-inhabited-emptiness-gives-emptiness
 : {X : 𝓀 Μ‡ }
 β†’ is-thinly-inhabited (is-empty X)
 β†’ is-empty X
thinly-inhabited-emptiness-gives-emptiness h =
 three-negations-imply-one (thinly-inhabited-gives-nonempty h)

thinly-inhabited-nonemptiness-gives-nonemptiness
 : {X : 𝓀 Μ‡ }
 β†’ is-thinly-inhabited (is-nonempty X)
 β†’ is-nonempty X
thinly-inhabited-nonemptiness-gives-nonemptiness {𝓀} {X} =
 thinly-inhabited-emptiness-gives-emptiness {𝓀} {is-empty X}

\end{code}

The following is a digression from our main aims. Recall that a type
is called discrete if it has decidable equality.

\begin{code}

Xβ†’πŸš-discreteness-criterion : {X : 𝓀 Μ‡ }
                           β†’ is-empty X + is-thinly-inhabited X
                           β†’ is-discrete (X β†’ 𝟚)
Xβ†’πŸš-discreteness-criterion (inl Ξ½) f g = inl (dfunext fe (Ξ» x β†’ 𝟘-elim (Ξ½ x)))
Xβ†’πŸš-discreteness-criterion (inr h) f g = retract-is-discrete
                                          (≃-gives-β–· (Οƒ _ , h))
                                          𝟚-is-discrete
                                          f g

Pβ†’πŸš-discreteness-criterion-necessity : {P : 𝓀 Μ‡ }
                                     β†’ is-prop P
                                     β†’ is-discrete (P β†’ 𝟚)
                                     β†’ Β¬ P + is-thinly-inhabited P
Pβ†’πŸš-discreteness-criterion-necessity {𝓀} {P} i Ξ΄ = Ο• (Ξ΄ Οƒβ‚€ σ₁)
 where
  Ο• : is-decidable (Οƒβ‚€ ＝ σ₁) β†’ Β¬ P + is-thinly-inhabited P
  Ο• (inl e) = inl (fact e)
   where
    fact : Οƒβ‚€ ＝ σ₁ β†’ Β¬ P
    fact e p = zero-is-not-one (ap (Ξ» f β†’ f p) e)
  Ο• (inr n) = inr (retraction-of-Οƒ-gives-thinly-inhabited i (Ξ³ , Ξ³Οƒ))
   where
    h : (f : P β†’ 𝟚) β†’ is-decidable (f ＝ Οƒβ‚€) β†’ 𝟚
    h f (inl _) = β‚€
    h f (inr _) = ₁

    Ξ³ : (P β†’ 𝟚) β†’ 𝟚
    Ξ³ f = h f (Ξ΄ f Οƒβ‚€)

    hβ‚€ : (d : is-decidable (Οƒβ‚€ ＝ Οƒβ‚€)) β†’ h Οƒβ‚€ d ＝ β‚€
    hβ‚€ (inl _) = refl
    hβ‚€ (inr d) = 𝟘-elim (d refl)

    h₁ : (d : is-decidable (σ₁ ＝ Οƒβ‚€)) β†’ h σ₁ d ＝ ₁
    h₁ (inl e) = 𝟘-elim (n (e ⁻¹))
    h₁ (inr _) = refl

    Ξ³Οƒ : Ξ³ ∘ Οƒ P ∼ id
    Ξ³Οƒ β‚€ = hβ‚€ (Ξ΄ Οƒβ‚€ Οƒβ‚€)
    Ξ³Οƒ ₁ = h₁ (Ξ΄ σ₁ Οƒβ‚€)

\end{code}

Added 25th March 2022. If every nonempty proposition is thinly inhabited,
then weak excluded middle holds. We use the following lemma to prove
this. Recall that the principle of weak excluded middle, which is
equivalent to De Morgan's Law, says that for every proposition P,
either ¬ P or ¬¬ P holds.

\begin{code}

thinly-inhabited-wem-lemma : (X : 𝓀 Μ‡ )
                           β†’ is-thinly-inhabited (X + is-empty X)
                           β†’ is-empty X + is-nonempty X
thinly-inhabited-wem-lemma X ti = II
 where
  Y = X + Β¬ X

  f : Y β†’ 𝟚
  f (inl _) = β‚€
  f (inr _) = ₁

  n : 𝟚
  n = inverse (Οƒ Y) ti f

  I : (k : 𝟚) β†’ n ＝ k β†’ Β¬ X + ¬¬ X
  I β‚€ e = inr Ο•
   where
    Iβ‚€ = f         ＝⟨ (inverses-are-sections (Οƒ Y) ti f)⁻¹ ⟩
         Οƒ Y n     ＝⟨ ap (Οƒ Y) e ⟩
         (Ξ» _ β†’ β‚€) ∎

    Ο• : ¬¬ X
    Ο• u = zero-is-not-one
           (β‚€         ＝⟨ (ap (Ξ» - β†’ - (inr u)) Iβ‚€)⁻¹ ⟩
            f (inr u) ＝⟨refl⟩
            ₁         ∎)

  I ₁ e = inl u
   where
    I₁ = f         ＝⟨ (inverses-are-sections (Οƒ Y) ti f)⁻¹ ⟩
         Οƒ Y n     ＝⟨ ap (Οƒ Y) e ⟩
         (Ξ» _ β†’ ₁) ∎

    u : Β¬ X
    u q = zero-is-not-one
           (β‚€         ＝⟨refl⟩
            f (inl q) ＝⟨ ap (Ξ» - β†’ - (inl q)) I₁ ⟩
            ₁         ∎)

  II : ¬ X + ¬¬ X
  II = I n refl

\end{code}

As promised above, thin inhabitedness is stronger than nonemptiness in
general, because WEM is not provable or disprovable, as it is true in
some models and false in others, and this is the main observation in
this file so far.

\begin{code}

irrefutable-props-are-thinly-inhabited-gives-WEM
 : ((P : 𝓀 Μ‡ ) β†’ is-prop P β†’ ¬¬ P β†’ is-thinly-inhabited P)
 β†’ typal-WEM 𝓀
irrefutable-props-are-thinly-inhabited-gives-WEM {𝓀} Ξ± = I
 where
  module _ (Q : 𝓀 Μ‡ ) (i : is-prop Q) where
   P = Q + Β¬ Q

   ν : ¬¬ P
   Ξ½ Ο• = Ο• (inr (Ξ» q β†’ Ο• (inl q)))

   h : is-thinly-inhabited P
   h = Ξ± P (decidability-of-prop-is-prop fe i) Ξ½

  I : typal-WEM 𝓀
  I = WEM-gives-typal-WEM fe (Ξ» Q i β†’ thinly-inhabited-wem-lemma Q (h Q i))

\end{code}

Nathanael Rosnik proved the above independently within a few
hours of difference here:
https://gist.github.com/nrosnick/922250ddcc6bd04272199f59443d7510

Conversely, weak excluded middle gives that every irrefutable
proposition is thinly inhabited, which we get from the above
discreteness criterion.

\begin{code}

typal-WEM-gives-Xβ†’πŸš-discreteness
 : typal-WEM 𝓀
 β†’ {X : 𝓀 Μ‡ } β†’ is-discrete (X β†’ 𝟚)
typal-WEM-gives-Xβ†’πŸš-discreteness {𝓀} wem {X} f g = I (wem (f ＝ g))
 where
  s : ¬¬ (f ＝ g) β†’ f ＝ g
  s Ο• = dfunext fe
         (Π-is-¬¬-stable
           (Ξ» x β†’ discrete-is-¬¬-separated 𝟚-is-discrete (f x) (g x))
           (¬¬-functor happly Ο•))

  I : Β¬ (f ＝ g) + ¬¬ (f ＝ g) β†’ is-decidable (f ＝ g)
  I (inl Ξ½) = inr Ξ½
  I (inr Ο•) = inl (s Ο•)

Xβ†’πŸš-discreteness-gives-irrefutable-props-are-thinly-inhabited
 : ((P : 𝓀 Μ‡ ) β†’ is-prop P β†’ is-discrete (P β†’ 𝟚))
 β†’ (P : 𝓀 Μ‡ ) β†’ is-prop P β†’ ¬¬ P β†’ is-thinly-inhabited P
Xβ†’πŸš-discreteness-gives-irrefutable-props-are-thinly-inhabited Ξ΄ P i Ξ½ =
 Cases (Pβ†’πŸš-discreteness-criterion-necessity i (Ξ΄ P i))
  (Ξ» (u : Β¬ P) β†’ 𝟘-elim (Ξ½ u))
  id

typal-WEM-gives-irrefutable-props-are-thinly-inhabited
 : typal-WEM 𝓀
 β†’ (P : 𝓀 Μ‡ ) β†’ is-prop P β†’ ¬¬ P β†’ is-thinly-inhabited P
typal-WEM-gives-irrefutable-props-are-thinly-inhabited wem =
 Xβ†’πŸš-discreteness-gives-irrefutable-props-are-thinly-inhabited
  (Ξ» P i β†’ typal-WEM-gives-Xβ†’πŸš-discreteness wem)

irrefutable-props-are-thinly-inhabited-iff-WEM
 : ((P : 𝓀 Μ‡ ) β†’ is-prop P β†’ ¬¬ P β†’ is-thinly-inhabited P)
 ↔ typal-WEM 𝓀
irrefutable-props-are-thinly-inhabited-iff-WEM =
 irrefutable-props-are-thinly-inhabited-gives-WEM ,
 typal-WEM-gives-irrefutable-props-are-thinly-inhabited

\end{code}

And so the discreteness of the type P β†’ 𝟚 for all propositions P is yet
another formulation of weak excluded middle.

\begin{code}

Pβ†’πŸš-discreteness-iff-WEM
 : ((P : 𝓀 Μ‡ ) β†’ is-prop P β†’ is-discrete (P β†’ 𝟚))
 ↔ typal-WEM 𝓀
Pβ†’πŸš-discreteness-iff-WEM =
 (irrefutable-props-are-thinly-inhabited-gives-WEM
   ∘ Xβ†’πŸš-discreteness-gives-irrefutable-props-are-thinly-inhabited) ,
 (Ξ» wem P i β†’ typal-WEM-gives-Xβ†’πŸš-discreteness wem)

\end{code}

End of addition and back to the past.

A minor observation, giving another instance of an implication
is-thinly-inhabited P β†’ P.

\begin{code}

thinly-inhabited-wem-special : (X : 𝓀 Μ‡ )
                             β†’ is-thinly-inhabited (is-empty X + is-nonempty X)
                             β†’ is-empty X + is-nonempty X
thinly-inhabited-wem-special X h =
 Cases (thinly-inhabited-wem-lemma (Β¬ X) h)
  inr
  (inl ∘ three-negations-imply-one)

\end{code}

Digression. A monad on propositions (or even a wild monad on all types?).

\begin{code}

module retraction-monad where

 Ξ· : {X : 𝓀 Μ‡ } β†’ X β†’ has-retraction (Οƒ X)
 Ξ· x = (Ξ» f β†’ f x) , (Ξ» n β†’ refl)

 _β™― : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
    β†’ (X β†’ has-retraction (Οƒ Y))
    β†’ (has-retraction (Οƒ X) β†’ has-retraction (Οƒ Y))
 _β™― {𝓀} {π“₯} {X} {Y} h (ρ , ρσ) = q
  where
   a : X β†’ (Y β†’ 𝟚) β†’ 𝟚
   a x = retraction-of (Οƒ Y) (h x)

   b : (x : X) (n : 𝟚) β†’ a x (Οƒ Y n) ＝ n
   b x = retraction-equation (Οƒ Y) (h x)

   u : (Y β†’ 𝟚) β†’ 𝟚
   u g = ρ (Ξ» x β†’ a x g)

   v : u ∘ Οƒ Y ∼ id
   v n = (u ∘ Οƒ Y) n           ＝⟨refl⟩
         ρ (Ξ» x β†’ a x (Οƒ Y n)) ＝⟨ ap ρ (dfunext fe (Ξ» x β†’ b x n)) ⟩
         ρ (Ξ» _ β†’ n)           ＝⟨refl⟩
         ρ (Οƒ X n)             ＝⟨ ρσ n ⟩
         n                     ∎

   q : has-retraction (Οƒ Y)
   q = u , v

 functor : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
         β†’ (X β†’ Y)
         β†’ (has-retraction (Οƒ X) β†’ has-retraction (Οƒ Y))
 functor f = (Ξ· ∘ f) β™―

 ΞΌ : (X : 𝓀 Μ‡ )
   β†’ has-retraction (Οƒ (has-retraction (Οƒ X)))
   β†’ has-retraction (Οƒ X)
 ΞΌ X = id β™―

\end{code}

TODO. It doesn't seem to be possible to give the structure of a monad
to is-thinly-inhabited.

Added 13th June 2024. The homotopy circle SΒΉ is thinly inhabited
because, as it is a connected 1-type, all functions SΒΉ β†’ 𝟚 are
constant as 𝟚 is a set. As another example, the type ℝ of Dedekind
reals is a set, but still there may be no function ℝ β†’ 𝟚 other than
the constant functions, because "all functions ℝ β†’ 𝟚 are continuous"
is a consistent axiom. But if a totally separated type (which is
necessarily a set) is thinly inhabited, then it must be a proposition.

Recall that x ＝₂ y is defined to mean that p x = p y for all p : X β†’ 𝟚,
that is, x and y satisfy the same boolean-valued properties. When
x ＝₂ y holds for all x and y in X, we say that X is connectedβ‚‚. And
recall that, in another extreme, when x ＝₂ y implies x ＝ y for all x
and y, we say that X is totally separated.

\begin{code}

open import TypeTopology.TotallySeparated
open import TypeTopology.DisconnectedTypes

thinly-inhabited-types-are-connectedβ‚‚ : {X : 𝓀 Μ‡ }
                                      β†’ is-thinly-inhabited X
                                      β†’ is-connectedβ‚‚ X
thinly-inhabited-types-are-connectedβ‚‚ {𝓀} {X} ti x y = I
 where
  e : 𝟚 ≃ (X β†’ 𝟚)
  e = Οƒ X , ti

  I : (p : X β†’ 𝟚) β†’ p x ＝ p y
  I p = p x                 ＝⟨ happly ((inverses-are-sections' e p)⁻¹) x ⟩
        ⌜ e ⌝ (⌜ e ⌝⁻¹ p) x ＝⟨refl⟩
        ⌜ e ⌝⁻¹ p           ＝⟨refl⟩
        ⌜ e ⌝ (⌜ e ⌝⁻¹ p) y ＝⟨ happly (inverses-are-sections' e p) y ⟩
        p y                 ∎

totally-separated-thinly-inhabited-types-are-props : {X : 𝓀 Μ‡ }
                                                   β†’ is-totally-separated X
                                                   β†’ is-thinly-inhabited X
                                                   β†’ is-prop X
totally-separated-thinly-inhabited-types-are-props ts ti x y = I
 where
  I : x ＝ y
  I = ts (thinly-inhabited-types-are-connectedβ‚‚ ti x y)

\end{code}

If replace the type 𝟚 by the type Ω of propositions in the notion of
thin inhabitedness, then we can replace the assumption
"is-totally-separated X" by "is-set X" to get the same conclusion
(exercise). And if we replace 𝟚 by some universe 𝓀, no assumption is
needed to conclude that thinly inhabited types are propositions:

\begin{code}

module universe-discussion where

 ΞΊ : (X : 𝓀 Μ‡ ) β†’ 𝓀 Μ‡ β†’ (X β†’ 𝓀 Μ‡ )
 ΞΊ X Y = Ξ» (_ : X) β†’ Y

 is-thinly-inhabited' : 𝓀 Μ‡ β†’ 𝓀 ⁺ Μ‡
 is-thinly-inhabited' X = is-equiv (ΞΊ X)

 thinly-inhabited'-types-are-props : {X : 𝓀 Μ‡ }
                                   β†’ is-thinly-inhabited' X
                                   β†’ is-prop X
 thinly-inhabited'-types-are-props {𝓀} {X} ti x y = III
  where
   e : 𝓀 Μ‡ ≃ (X β†’ 𝓀 Μ‡ )
   e = ΞΊ X , ti

   I : (p : X β†’ 𝓀 Μ‡ ) β†’ p x ＝ p y
   I p = p x                 ＝⟨ happly ((inverses-are-sections' e p)⁻¹) x ⟩
         ⌜ e ⌝ (⌜ e ⌝⁻¹ p) x ＝⟨refl⟩
         ⌜ e ⌝⁻¹ p           ＝⟨refl⟩
         ⌜ e ⌝ (⌜ e ⌝⁻¹ p) y ＝⟨ happly (inverses-are-sections' e p) y ⟩
         p y                 ∎

   II : (x ＝ x) ＝ (x ＝ y)
   II = I (x ＝_)

   III : x ＝ y
   III = idtofun' II refl

 Ξ· : {X : 𝓀 Μ‡ } β†’ is-prop X β†’ X β†’ is-thinly-inhabited' X
 Ξ· {𝓀} {X} i xβ‚€ = qinvs-are-equivs (ΞΊ X) (s , sΞΊ , ΞΊs)
  where
   s : (X β†’ 𝓀 Μ‡ ) β†’ 𝓀 Μ‡
   s A = A xβ‚€

   sκ : s ∘ κ X ∼ id
   sΞΊ Y = refl

   κs : κ X ∘ s ∼ id
   ΞΊs A = dfunext fe (Ξ» x β†’ ap A (i xβ‚€ x))

 thinly-inhabited'-gives-nonempty : {X : 𝓀 Μ‡ }
                                  β†’ is-thinly-inhabited' X
                                  β†’ is-nonempty X
 thinly-inhabited'-gives-nonempty {𝓀} {X} ti Ξ½ = III
  where
   e : 𝓀 Μ‡ ≃ (X β†’ 𝓀 Μ‡ )
   e = ΞΊ X , ti

   I : ⌜ e ⌝⁻¹  (⌜ e ⌝ πŸ™) ＝ ⌜ e ⌝⁻¹  (⌜ e ⌝ 𝟘)
   I = ap (⌜ e ⌝⁻¹) (⌜ e ⌝ πŸ™ ＝⟨ dfunext fe (Ξ» x β†’ 𝟘-elim (Ξ½ x)) ⟩
                     ⌜ e ⌝ 𝟘 ∎)

   II = πŸ™                 ＝⟨ (inverses-are-retractions' e πŸ™)⁻¹ ⟩
        ⌜ e ⌝⁻¹ (⌜ e ⌝ πŸ™) ＝⟨ I ⟩
        ⌜ e ⌝⁻¹ (⌜ e ⌝ 𝟘) ＝⟨ inverses-are-retractions' e 𝟘 ⟩
        𝟘                 ∎

   III : 𝟘 {𝓀₀}
   III = 𝟘-elim (idtofun' II ⋆)

\end{code}

TODO (done below). Derive a constructive taboo from the hypothesis

      (P : 𝓀 Μ‡ ) β†’ is-prop P β†’ is-thinly-inhabited P β†’ P.

The difficulty, of course, is to come up with a type P which we can
prove to be thinly inhabited but (we can't prove to be pointed and)
whose pointedness would give a constructive taboo.

Added 16th October 2026. We now come back to the original notion of
thin inhabitedness studied in this file, and solve the above TODO. The
taboo is that weak excluded middle implies excluded middle.

\begin{code}

WEM-implies-EM : βˆ€ 𝓀 β†’ 𝓀 ⁺ Μ‡
WEM-implies-EM 𝓀 = typal-WEM 𝓀 β†’ EM 𝓀

\end{code}

We choose the typal version, rather than the propositional version,
for technical convenience. But notice that it doesn't make any
mathematical difference, because, as we have shown in
UF.ClassicalLogic, typal WEM is logically equivalent to propositional WEM.

This can be considered as a sort of taboo because weak excluded middle
holds in models in which excluded middle fails, the simplest example
being sheaves over the two-point space with one open point. Weak
excluded middle is De Morgan's law, and the toposes that satisfy it are
studied in

   P.T. Johnstone. Conditions related to de Morgan's law. Applications
   of Sheaves, Lecture Notes in Mathematics, Vol 753, Springer, 1979,
   pp. 479-491. https://doi.org/10.1007/BFb0061829

We first show that thin inhabitedness amounts to Ξ -compactness
together with nonemptiness. We repeat the definition of Ξ -compactness,
rather than import it from TypeTopology.WeaklyCompactTypes, because
that module assumes propositional truncations and this one doesn't. One
direction holds for arbitrary types, and for the other we need a
proposition, as in the above case of a retraction of Οƒ.

\begin{code}

is-Ξ -compact : 𝓀 Μ‡ β†’ 𝓀 Μ‡
is-Ξ -compact X = (p : X β†’ 𝟚) β†’ is-decidable ((x : X) β†’ p x ＝ ₁)

thinly-inhabited-types-are-Ξ -compact
 : {X : 𝓀 Μ‡ }
 β†’ is-thinly-inhabited X
 β†’ is-Ξ -compact X
thinly-inhabited-types-are-Ξ -compact {𝓀} {X} ti p = I (constancy ti p)
 where
  I : (Ξ£ n κž‰ 𝟚 , p ＝ (Ξ» _ β†’ n)) β†’ is-decidable ((x : X) β†’ p x ＝ ₁)
  I (β‚€ , e) = inr (Ξ» (Ξ± : (x : X) β†’ p x ＝ ₁)
                     β†’ thinly-inhabited-gives-nonempty ti
                        (Ξ» x β†’ zero-is-not-one
                                (β‚€   ＝⟨ (happly e x)⁻¹ ⟩
                                 p x ＝⟨ α x ⟩
                                 ₁   ∎)))
  I (₁ , e) = inl (happly e)

Ξ -compact-nonempty-props-are-thinly-inhabited
 : {P : 𝓀 Μ‡ }
 β†’ is-prop P
 β†’ is-Ξ -compact P
 β†’ is-nonempty P
 β†’ is-thinly-inhabited P
Ξ -compact-nonempty-props-are-thinly-inhabited {𝓀} {P} i c Ξ½ =
 retraction-of-Οƒ-gives-thinly-inhabited i (ρ , ρσ)
 where
  h : (f : P β†’ 𝟚) β†’ is-decidable ((x : P) β†’ f x ＝ ₁) β†’ 𝟚
  h f (inl _) = ₁
  h f (inr _) = β‚€

  ρ : (P β†’ 𝟚) β†’ 𝟚
  ρ f = h f (c f)

  hβ‚€ : (d : is-decidable ((x : P) β†’ Οƒβ‚€ x ＝ ₁)) β†’ h Οƒβ‚€ d ＝ β‚€
  hβ‚€ (inl Ξ±) = 𝟘-elim (Ξ½ (Ξ» p β†’ zero-is-not-one (Ξ± p)))
  hβ‚€ (inr _) = refl

  h₁ : (d : is-decidable ((x : P) β†’ σ₁ x ＝ ₁)) β†’ h σ₁ d ＝ ₁
  h₁ (inl _) = refl
  h₁ (inr u) = 𝟘-elim (u (Ξ» _ β†’ refl))

  ρσ : ρ ∘ Οƒ P ∼ id
  ρσ β‚€ = hβ‚€ (c Οƒβ‚€)
  ρσ ₁ = h₁ (c σ₁)

thinly-inhabited-iff-Ξ -compact-and-nonempty
 : {P : 𝓀 Μ‡ }
 β†’ is-prop P
 β†’ is-thinly-inhabited P
 ↔ (is-Ξ -compact P Γ— is-nonempty P)
thinly-inhabited-iff-Ξ -compact-and-nonempty i =
 (Ξ» ti β†’ thinly-inhabited-types-are-Ξ -compact ti ,
         thinly-inhabited-gives-nonempty ti) ,
 (Ξ» (c , Ξ½) β†’ Ξ -compact-nonempty-props-are-thinly-inhabited i c Ξ½)

\end{code}

In particular, the principle that all irrefutable propositions are
Ξ -compact amounts to weak excluded middle.

\begin{code}

irrefutable-props-are-Ξ -compact-iff-WEM
 : ((P : 𝓀 Μ‡ ) β†’ is-prop P β†’ ¬¬ P β†’ is-Ξ -compact P)
 ↔ typal-WEM 𝓀
irrefutable-props-are-Ξ -compact-iff-WEM =
 (Ξ» c β†’ irrefutable-props-are-thinly-inhabited-gives-WEM
         (Ξ» P i Ξ½ β†’ Ξ -compact-nonempty-props-are-thinly-inhabited
                     i (c P i Ξ½) Ξ½)) ,
 (Ξ» wem P i Ξ½ β†’ thinly-inhabited-types-are-Ξ -compact
                 (typal-WEM-gives-irrefutable-props-are-thinly-inhabited
                   wem P i Ξ½))

\end{code}

We now name the property we want to characterize.

\begin{code}

Thinly-Inhabited-Props-Are-Pointed : βˆ€ 𝓀 β†’ 𝓀 ⁺ Μ‡
Thinly-Inhabited-Props-Are-Pointed 𝓀 =
  (P : 𝓀 Μ‡ )
 β†’ is-prop P
 β†’ is-thinly-inhabited P
 β†’ P

\end{code}

That thinly inhabited propositions are pointed follows from double
negation elimination, because thinly inhabited types are nonempty, and
so the hypothesis is classically true, which means that no
anti-classical taboo can follow from it.

\begin{code}

DNE-gives-thinly-inhabited-props-are-pointed
 : DNE 𝓀
 β†’ Thinly-Inhabited-Props-Are-Pointed 𝓀
DNE-gives-thinly-inhabited-props-are-pointed dne P i ti =
 dne P i (thinly-inhabited-gives-nonempty ti)

\end{code}

By the above characterization of thin inhabitedness, the hypothesis
says precisely that Ξ -compact propositions are decidable. We name this
property.

\begin{code}

Ξ -Compact-Props-Are-Decidable : βˆ€ 𝓀 β†’ 𝓀 ⁺ Μ‡
Ξ -Compact-Props-Are-Decidable 𝓀 =
   (P : 𝓀 Μ‡ )
 β†’ is-prop P
 β†’ is-Ξ -compact P
 β†’ is-decidable P

thinly-inhabited-props-are-pointed-iff-Ξ -compact-props-are-decidable
 : Thinly-Inhabited-Props-Are-Pointed 𝓀
 ↔ Ξ -Compact-Props-Are-Decidable 𝓀
thinly-inhabited-props-are-pointed-iff-Ξ -compact-props-are-decidable {𝓀} =
 (f , g)
 where
  f : Thinly-Inhabited-Props-Are-Pointed 𝓀
    β†’ Ξ -Compact-Props-Are-Decidable 𝓀
  f Ξ± P i c = I (c Οƒβ‚€)
   where
    I : is-decidable ((x : P) β†’ Οƒβ‚€ x ＝ ₁) β†’ is-decidable P
    I (inl Ξ²) = inr (Ξ» p β†’ zero-is-not-one (Ξ² p))
    I (inr u) = inl (Ξ± P i (Ξ -compact-nonempty-props-are-thinly-inhabited
                            i c Ξ½))
     where
      Ξ½ : is-nonempty P
      Ξ½ Ο• = u (Ξ» p β†’ 𝟘-elim (Ο• p))

  g : Ξ -Compact-Props-Are-Decidable 𝓀
    β†’ Thinly-Inhabited-Props-Are-Pointed 𝓀
  g Ξ² P i ti = I (Ξ² P i (thinly-inhabited-types-are-Ξ -compact ti))
   where
    I : is-decidable P β†’ P
    I (inl p) = p
    I (inr u) = 𝟘-elim (thinly-inhabited-gives-nonempty ti u)

\end{code}

Equivalently, by the discreteness criterion given above, the
hypothesis says that the discreteness of P β†’ 𝟚 gives the decidability
of P. This reverses the implication from the decidability of P to the
discreteness of P β†’ 𝟚, which is the motivation for this file, and we
come back to this below.

\begin{code}

Pβ†’πŸš-Discreteness-Gives-Decidability : βˆ€ 𝓀 β†’ 𝓀 ⁺ Μ‡
Pβ†’πŸš-Discreteness-Gives-Decidability 𝓀 =
 (P : 𝓀 Μ‡ ) β†’ is-prop P β†’ is-discrete (P β†’ 𝟚) β†’ is-decidable P

thinly-inhabited-props-are-pointed-iff-Pβ†’πŸš-discreteness-gives-decidability
 : Thinly-Inhabited-Props-Are-Pointed 𝓀
 ↔ Pβ†’πŸš-Discreteness-Gives-Decidability 𝓀
thinly-inhabited-props-are-pointed-iff-Pβ†’πŸš-discreteness-gives-decidability
 {𝓀} = (f , g)
 where
  f : Thinly-Inhabited-Props-Are-Pointed 𝓀
    β†’ Pβ†’πŸš-Discreteness-Gives-Decidability 𝓀
  f Ξ± P i Ξ΄ = Cases (Pβ†’πŸš-discreteness-criterion-necessity i Ξ΄)
               inr
               (Ξ» ti β†’ inl (Ξ± P i ti))

  g : Pβ†’πŸš-Discreteness-Gives-Decidability 𝓀
    β†’ Thinly-Inhabited-Props-Are-Pointed 𝓀
  g Ξ² P i ti = I (Ξ² P i (Xβ†’πŸš-discreteness-criterion (inr ti)))
   where
    I : is-decidable P β†’ P
    I (inl p) = p
    I (inr u) = 𝟘-elim (thinly-inhabited-gives-nonempty ti u)

\end{code}

And here is the derivation of the taboo. Under weak excluded middle
every irrefutable proposition is thinly inhabited, and so the
hypothesis turns weak excluded middle into double negation elimination,
and hence into excluded middle.

\begin{code}

thinly-inhabited-props-are-pointed-gives-WEM-implies-EM
 : Thinly-Inhabited-Props-Are-Pointed 𝓀
 β†’ WEM-implies-EM 𝓀
thinly-inhabited-props-are-pointed-gives-WEM-implies-EM {𝓀} Ξ± wem =
 DNE-gives-EM fe I
 where
  I : DNE 𝓀
  I P i Ξ½ = Ξ± P i
             (typal-WEM-gives-irrefutable-props-are-thinly-inhabited
               wem P i Ξ½)

\end{code}

And this is all that the hypothesis gives, in the sense that the
hypothesis and weak excluded middle together are equivalent to excluded
middle.

\begin{code}

thinly-inhabited-props-are-pointed-and-WEM-iff-EM
 : (Thinly-Inhabited-Props-Are-Pointed 𝓀 Γ— typal-WEM 𝓀) ↔ EM 𝓀
thinly-inhabited-props-are-pointed-and-WEM-iff-EM {𝓀} = (f , g)
 where
  f : Thinly-Inhabited-Props-Are-Pointed 𝓀 Γ— typal-WEM 𝓀 β†’ EM 𝓀
  f (Ξ± , wem) = thinly-inhabited-props-are-pointed-gives-WEM-implies-EM Ξ± wem

  g : EM 𝓀 β†’ Thinly-Inhabited-Props-Are-Pointed 𝓀 Γ— typal-WEM 𝓀
  g em = DNE-gives-thinly-inhabited-props-are-pointed (EM-gives-DNE em) ,
         (Ξ» A β†’ em (Β¬ A) (negations-are-props fe))

\end{code}

And so the hypothesis gives excluded middle if and only if it gives
weak excluded middle.

\begin{code}

thinly-inhabited-props-are-pointed-gives-EM-iff-gives-WEM
 : (Thinly-Inhabited-Props-Are-Pointed 𝓀 β†’ EM 𝓀)
 ↔ (Thinly-Inhabited-Props-Are-Pointed 𝓀 β†’ typal-WEM 𝓀)
thinly-inhabited-props-are-pointed-gives-EM-iff-gives-WEM {𝓀} = (f , g)
 where
  f : (Thinly-Inhabited-Props-Are-Pointed 𝓀 β†’ EM 𝓀)
    β†’ Thinly-Inhabited-Props-Are-Pointed 𝓀 β†’ typal-WEM 𝓀
  f Ο• Ξ± A = Ο• Ξ± (Β¬ A) (negations-are-props fe)

  g : (Thinly-Inhabited-Props-Are-Pointed 𝓀 β†’ typal-WEM 𝓀)
    β†’ Thinly-Inhabited-Props-Are-Pointed 𝓀 β†’ EM 𝓀
  g Ξ³ Ξ± = thinly-inhabited-props-are-pointed-gives-WEM-implies-EM Ξ± (Ξ³ Ξ±)

\end{code}

We haven't managed to derive weak excluded middle from the hypothesis,
and by the above this is the same as deriving excluded middle from it.
As excluded middle gives the hypothesis, either of these would show
that the hypothesis and excluded middle are equivalent.

This also answers the question that motivates this file. Recall from
the discussion at the end of Ordinals.InductiveRecursiveCodesInterpretations
the implications

 (0) if P is decidable then P β†’ 𝟚 is discrete,
 (1) if P β†’ 𝟚 is discrete then Β¬ P is decidable,

and the question of whether they can be reversed. Read as principles
about all propositions, the discreteness of P β†’ 𝟚 and the decidability
of Β¬ P are both weak excluded middle, as shown above, and the
decidability of P is excluded middle. So (1) can be reversed as a
principle, although not for an individual proposition, because the
proof that P β†’ 𝟚 is discrete under weak excluded middle uses it for
propositions other than P. The reversal of (0) as a principle says that
weak excluded middle implies excluded middle, which is the taboo above,
and for an individual proposition it is the hypothesis itself. So, as a
principle, the discreteness of P β†’ 𝟚 is not strictly between the
decidability of P and that of Β¬ P, because it is equivalent to the
decidability of Β¬ P, and what is missing for the decidability of P is
the implication from weak excluded middle to excluded middle. We don't
know whether, conversely, this implication gives the hypothesis.

Finally, we discuss the original question, which was to find a type P
that we can prove to be thinly inhabited and whose pointedness gives a
constructive taboo. Anything that follows from the pointedness of such
a P is irrefutable, because thinly inhabited types are nonempty.

\begin{code}

consequences-of-thinly-inhabited-props-are-irrefutable
 : {P : 𝓀 Μ‡ } {X : π“₯ Μ‡ }
 β†’ is-thinly-inhabited P
 β†’ (P β†’ X)
 β†’ ¬¬ X
consequences-of-thinly-inhabited-props-are-irrefutable ti f =
 ¬¬-functor f (thinly-inhabited-gives-nonempty ti)

\end{code}

So such a P can give only irrefutable statements, and in particular no
statement whose negation is consistent. The most it could give is one
that is irrefutable but not provable, and we don't have such a P.