Martin Escardo, 24th March 2022
with minor improvements and additions June 2024.

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

\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

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}

We now come back to the original notion of thin inhabitedness studied
in this file.

TODO. 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.