Martin Escardo, March 2022

This generalizes the 2018 file OrdinalNotationInterpretation1.

A Tarski universe E of ordinal codes with two related decoding
functions Δ and Κ (standing for "discrete" and "compact"

Roughly speaking, E gives ordinal codes or expressions denoting
infinite ordinals. The expressions themselves are infinitary.

An ordinal is a type equipped with an order _≺_ that satisfies
suitable properties, which in particular imply that the type is a set
in the sense of HoTT/UF. The adopted notion of ordinal is that of the
HoTT book.

For a code ν : E, we have an ordinal Δ ν, which is discrete (has
decidable equality).

For a code ν : E, we have an ordinal Κ ν, which is compact (or
"searchable"). More than that, every complemented subset of Κ ν is
either empty or has a minimal element.

There is an embedding ι : Δ ν → Κ ν which is order preserving and
reflecting, and whose image has empty complement. The assumption that
it is a bijection implies LPO.

This extends and generalizes OrdinalNotationInterpretation1.lagda, for
which slides for a talk are available at which may well serve
as an introduction to this file. The main difference is that the
ordinal expressions considered there amount to a W type, whereas the
ones considered here amount to an inductive-recursive type,
generalizing that, which is explained in these slides

This is a draft version that needs polishing and more explanation.


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

open import MLTT.Spartan
open import UF.FunExt

module Ordinals.NotationInterpretation2 (fe : FunExt) where

 fe₀ = fe 𝓤₀ 𝓤₀

open import CoNaturals.Type
open import MLTT.Two-Properties
open import Naturals.Binary hiding (_+_)
open import Notation.CanonicalMap hiding (ι)
open import Ordinals.Arithmetic fe
open import Ordinals.Closure fe
open import Ordinals.Equivalence
open import Ordinals.Injectivity
open import Ordinals.ToppedArithmetic fe
open import Ordinals.ToppedType fe
open import Ordinals.Type
open import Ordinals.Underlying
open import Taboos.LPO fe
open import Taboos.WLPO
open import TypeTopology.CompactTypes
open import TypeTopology.ConvergentSequenceHasInf
open import TypeTopology.Density
open import TypeTopology.InfProperty
open import TypeTopology.PropInfTychonoff fe
open import TypeTopology.PropTychonoff fe
open import TypeTopology.SigmaDiscreteAndTotallySeparated
open import UF.Base
open import UF.Embeddings
open import UF.DiscreteAndSeparated
open import UF.Equiv
open import UF.PairFun
open import UF.Retracts
open import UF.Subsingletons
open import UF.Subsingletons-FunExt


We define E and Δ by simultaneous induction. The type Ordᵀ is that of
ordinals with a top element (classically, successor ordinals). Recall
that ⟪ α ⟫ is the underlying type of α : Ordᵀ.


data E : 𝓤₀ ̇
Δ : E  Ordᵀ

data E where
 ⌜𝟙⌝   : E
 ⌜ω+𝟙⌝ : E
 _⌜+⌝_ : E  E  E
 _⌜×⌝_ : E  E  E
 ⌜Σ⌝   : (ν : E)  ( Δ ν   E)  E

Δ ⌜𝟙⌝         = 𝟙ᵒ
Δ ⌜ω+𝟙⌝       = succₒ ω
Δ (ν₀ ⌜+⌝ ν₁) = Δ ν₀ +ᵒ Δ ν₁
Δ (ν₀ ⌜×⌝ ν₁) = Δ ν₀ ×ᵒ Δ ν₁
Δ (⌜Σ⌝ ν A)   =  (Δ ν) (Δ  A)


All ordinals in the image of Δ are retracts of ℕ (and hence


Δ-retract-of-ℕ : (ν : E)  retract  Δ ν  of 
Δ-retract-of-ℕ ⌜𝟙⌝         =  _  ) ,  _  0) , 𝟙-is-prop 
Δ-retract-of-ℕ ⌜ω+𝟙⌝       = ≃-gives-◁ ℕ-plus-𝟙
Δ-retract-of-ℕ (ν₀ ⌜+⌝ ν₁) = Σ-retract-of-ℕ
                              (dep-cases  _  Δ-retract-of-ℕ ν₀)
                                          _  Δ-retract-of-ℕ ν₁))
Δ-retract-of-ℕ (ν₀ ⌜×⌝ ν₁) = Σ-retract-of-ℕ
                              (Δ-retract-of-ℕ ν₀)
                               _  Δ-retract-of-ℕ ν₁)
Δ-retract-of-ℕ (⌜Σ⌝ ν A)   = Σ-retract-of-ℕ
                              (Δ-retract-of-ℕ ν)
                               x  Δ-retract-of-ℕ (A x))

Hence all ordinals in the image of Δ are discrete (have decidable equality):


Δ-is-discrete : (ν : E)  is-discrete  Δ ν 
Δ-is-discrete ν = retract-is-discrete (Δ-retract-of-ℕ ν) ℕ-is-discrete


A stronger result is that the ordinals in the image of Δ are trichotomous:


Δ-is-trichotomous : (ν : E)  is-trichotomous [ Δ ν ]
Δ-is-trichotomous ⌜𝟙⌝         = 𝟙ₒ-is-trichotomous
Δ-is-trichotomous ⌜ω+𝟙⌝       = succₒ-is-trichotomous ω ω-is-trichotomous
Δ-is-trichotomous (ν₀ ⌜+⌝ ν₁) = +ᵒ-is-trichotomous (Δ ν₀) (Δ ν₁)
                                  (Δ-is-trichotomous ν₀)
                                  (Δ-is-trichotomous ν₁)
Δ-is-trichotomous (ν₀ ⌜×⌝ ν₁) = ×ᵒ-is-trichotomous (Δ ν₀) (Δ ν₁)
                                  (Δ-is-trichotomous ν₀)
                                  (Δ-is-trichotomous ν₁)
Δ-is-trichotomous (⌜Σ⌝ ν A)   = ∑-is-trichotomous (Δ ν) (Δ  A)
                                 (Δ-is-trichotomous ν)
                                  x  Δ-is-trichotomous (A x))

Now we define Κ, ι, ι-is-embedding by simultaneous induction.


Κ : E  Ordᵀ
ι : (ν : E)   Δ ν    Κ ν 
ι-is-embedding : (ν : E)  is-embedding (ι ν)


Before completing the induction, we define the following abbreviation:


j : (ν : E)   Δ ν    Κ ν 
j ν = ι ν , ι-is-embedding ν


We use the following auxiliary extension constructions, illustrated by
this diagram:

                   ι ν
          ⟨ Δ ν ⟩  ⟶ ⟨ Κ ν ⟩
              |           .
              |           .
           A  |           .  (K ∘ A) ↗ j ν
              |           .
              ↓           ↓
              E    ⟶   Ordᵀ

See the files ToppedOrdinalArithmetic and InjectiveTypes for details.


open topped-ordinals-injectivity fe

𝓚 : (ν : E)  ( Δ ν   E)   Κ ν   Ordᵀ
𝓚 ν A = (Κ  A)  (ι ν , ι-is-embedding ν)


Explicitly, the underlying set of this ordinal is given as follows in
the file InjectiveTypes:


underlying-set-of-𝓚 : (ν : E) (A :  Δ ν   E) (y :  Κ ν )
                      𝓚 ν A y   (Π (x , _)  fiber (ι ν) y ,  Κ (A x) )
underlying-set-of-𝓚 ν A y = refl


The above gives an extension up to ordinal equivalence


module Κ-extension (ν : E) (A :  Δ ν   E) where

 ϕ : (x :  Δ ν )  [ 𝓚 ν A (ι ν x) ] ≃ₒ [ Κ (A x) ]
 ϕ = ↗-propertyₒ (Κ  A) (j ν)

 φ : (x :  Δ ν )   𝓚 ν A (ι ν x)    Κ (A x) 
 φ x = ≃ₒ-to-fun [ 𝓚 ν A (ι ν x) ] [ Κ (A x) ] (ϕ x)

 γ : (x :  Δ ν )   Κ (A x)    𝓚 ν A (ι ν x) 
 γ x = ≃ₒ-to-fun⁻¹ [ 𝓚 ν A (ι ν x) ] [ Κ (A x) ] (ϕ x)

 φ-is-equiv : (x :  Δ ν )  is-equiv (φ x)
 φ-is-equiv x = ≃ₒ-to-fun-is-equiv [ 𝓚 ν A (ι ν x) ] [ Κ (A x) ] (ϕ x)

 γ-is-equiv : (x :  Δ ν )  is-equiv (γ x)
 γ-is-equiv x = ≃ₒ-to-fun⁻¹-is-equiv [ 𝓚 ν A (ι ν x) ] [ Κ (A x) ] (ϕ x)

Κ ⌜𝟙⌝         = 𝟙ᵒ
Κ ⌜ω+𝟙⌝       = ℕ∞ᵒ
Κ (ν₀ ⌜+⌝ ν₁) = Κ ν₀ +ᵒ Κ ν₁
Κ (ν₀ ⌜×⌝ ν₁) = Κ ν₀ ×ᵒ Κ ν₁
Κ (⌜Σ⌝ ν A)   =  (Κ ν) (𝓚 ν A)

ι ⌜𝟙⌝         = id
ι ⌜ω+𝟙⌝       = ι𝟙
ι (ν₀ ⌜+⌝ ν₁) = pair-fun id (dep-cases  _  ι ν₀)  _  ι ν₁))
ι (ν₀ ⌜×⌝ ν₁) = pair-fun (ι ν₀)  _  ι ν₁)
ι (⌜Σ⌝ ν A)   = pair-fun (ι ν)  x  γ x  ι (A x))
  open Κ-extension ν A

ι-is-embedding ⌜𝟙⌝         = id-is-embedding
ι-is-embedding ⌜ω+𝟙⌝       = ι𝟙-is-embedding fe₀
ι-is-embedding (ν₀ ⌜+⌝ ν₁) = pair-fun-is-embedding
                              (dep-cases  _  ι ν₀)  _  ι ν₁))
                              (dep-cases  _  ι-is-embedding ν₀)
                                          _  ι-is-embedding ν₁))
ι-is-embedding (ν₀ ⌜×⌝ ν₁) = pair-fun-is-embedding _ _
                              (ι-is-embedding ν₀)
                               _  ι-is-embedding ν₁)
ι-is-embedding (⌜Σ⌝ ν A)   = pair-fun-is-embedding _ _
                              (ι-is-embedding ν)
                               x  ∘-is-embedding
                                      (ι-is-embedding (A x))
                                      (equivs-are-embeddings (γ x) (γ-is-equiv x)))
  open Κ-extension ν A


This completes the definitions of Κ, ι and ι-is-embedding.

The important fact about the Κ interpretation is that the ordinals in
its image have the least element property for complemented subsets, and,
in particular, they are compact.


module _ (pe : propext 𝓤₀) where

 K-has-infs-of-complemented-subsets : (ν : E)
                                     has-infs-of-complemented-subsets (Κ ν)
 𝓚-has-infs-of-complemented-subsets : (ν : E) (A :  Δ ν   E) (x :  Κ ν )
                                     has-infs-of-complemented-subsets (𝓚 ν A x)

 K-has-infs-of-complemented-subsets ⌜𝟙⌝         =
 K-has-infs-of-complemented-subsets ⌜ω+𝟙⌝       =
  ℕ∞ᵒ-has-infs-of-complemented-subsets pe
 K-has-infs-of-complemented-subsets (ν₀ ⌜+⌝ ν₁) =
  ∑-has-infs-of-complemented-subsets pe
    (cases  _  Κ ν₀)  _  Κ ν₁))
       _  K-has-infs-of-complemented-subsets ν₀)
       _  K-has-infs-of-complemented-subsets ν₁))
 K-has-infs-of-complemented-subsets (ν₀ ⌜×⌝ ν₁) =
   ∑-has-infs-of-complemented-subsets pe
     (Κ ν₀)
      _  Κ ν₁)
     (K-has-infs-of-complemented-subsets ν₀)
      _  K-has-infs-of-complemented-subsets ν₁)
 K-has-infs-of-complemented-subsets (⌜Σ⌝ ν A) =
   ∑-has-infs-of-complemented-subsets pe (Κ ν) (𝓚 ν A)
     (K-has-infs-of-complemented-subsets ν)
     (𝓚-has-infs-of-complemented-subsets ν A)

 𝓚-has-infs-of-complemented-subsets ν A x =
    (ι-is-embedding ν x)
     {(x , _)} y z  y ≺⟨ Κ (A x)  z)
     (x , _)  K-has-infs-of-complemented-subsets (A x))


And, as discussed above, as a corollary we get that the ordinals in
the image of Κ are compact:


 Κ-Compact : {𝓥 : Universe} (ν : E)
            is-Compact  Κ ν  {𝓥}
 Κ-Compact ν = has-inf-gives-Compact _ (K-has-infs-of-complemented-subsets ν)

 𝓚-Compact : {𝓥 : Universe} (ν : E) (A :  Δ ν   E) (x :  Κ ν )
             is-Compact  𝓚 ν A x  {𝓥}
 𝓚-Compact ν A x = has-inf-gives-Compact _ (𝓚-has-infs-of-complemented-subsets ν A x)


The embedding of the Δ interpretation into the Κ interpretation is
order-preserving, order-reflecting, and dense (its image has empty


ι-is-order-preserving : (ν : E) (x y :  Δ ν )
                           x ≺⟨ Δ ν      y
                       ι ν x ≺⟨ Κ ν  ι ν y
ι-is-order-preserving ⌜𝟙⌝         = λ x y l  l
ι-is-order-preserving ⌜ω+𝟙⌝       = ι𝟙ᵒ-is-order-preserving
ι-is-order-preserving (ν₀ ⌜+⌝ ν₁) = pair-fun-is-order-preserving
                                     (cases  _  Δ ν₀)  _  Δ ν₁))
                                     (cases  _  Κ ν₀)  _  Κ ν₁))
                                     (dep-cases  _  ι ν₀)  _  ι ν₁))
                                      x y l  l)
                                     (dep-cases  _  ι-is-order-preserving ν₀)
                                                 _  ι-is-order-preserving ν₁))
ι-is-order-preserving (ν₀ ⌜×⌝ ν₁) = pair-fun-is-order-preserving
                                     (Δ ν₀)
                                     (Κ ν₀)
                                      _  Δ ν₁)
                                      _  Κ ν₁)
                                     (ι ν₀)
                                      _  ι ν₁)
                                     (ι-is-order-preserving ν₀)
                                      _  ι-is-order-preserving ν₁)
ι-is-order-preserving (⌜Σ⌝ ν A)   = pair-fun-is-order-preserving
                                     (Δ ν)
                                     (Κ ν)
                                     (Δ  A)
                                     (𝓚 ν A)
                                     (ι ν)
                                      x  γ x  ι (A x))
                                     (ι-is-order-preserving ν)
  open Κ-extension ν A

  IH : (x :  Δ ν ) (y z :  Δ (A x) )
              y ≺⟨ Δ (A x)  z
      ι (A x) y ≺⟨ Κ (A x)  ι (A x) z
  IH x = ι-is-order-preserving (A x)

  f : (x :  Δ ν ) (y z :  Δ (A x) )
     ι (A x) y        ≺⟨ Κ (A x)         ι (A x) z
      γ x (ι (A x) y) ≺⟨ 𝓚 ν A (ι ν x)  γ x (ι (A x) z)
  f x y z = inverses-of-order-equivs-are-order-preserving [ 𝓚 ν A (ι ν x) ] [ Κ (A x) ]
             (≃ₒ-to-fun-is-order-equiv [ 𝓚 ν A (ι ν x) ] [ Κ (A x) ] (ϕ x)) _ _

  g : (x :  Δ ν ) (y z :  Δ (A x) )
     y               ≺⟨ Δ (A x)         z
     γ x (ι (A x) y) ≺⟨ 𝓚 ν A (ι ν x)  γ x (ι (A x) z)
  g x y z l = f x y z (IH x y z l)

ι-is-order-reflecting : (ν : E) (x y :  Δ ν )
                       ι ν x ≺⟨ Κ ν  ι ν y
                           x ≺⟨ Δ ν      y
ι-is-order-reflecting ⌜𝟙⌝        = λ x y l  l
ι-is-order-reflecting ⌜ω+𝟙⌝      = ι𝟙ᵒ-is-order-reflecting
ι-is-order-reflecting (ν₀ ⌜+⌝ ν₁) =  pair-fun-is-order-reflecting
                                      (cases  _  Δ ν₀)  _  Δ ν₁))
                                      (cases  _  Κ ν₀)  _  Κ ν₁))
                                      (dep-cases  _  ι ν₀)  _  ι ν₁))
                                       x y l  l)
                                      (dep-cases  _  ι-is-order-reflecting ν₀)
                                                  _  ι-is-order-reflecting ν₁))
ι-is-order-reflecting (ν₀ ⌜×⌝ ν₁) = pair-fun-is-order-reflecting
                                     (Δ ν₀)
                                     (Κ ν₀)
                                      _  Δ ν₁)
                                      _  Κ ν₁)
                                     (ι ν₀)
                                      _  ι ν₁)
                                     (ι-is-order-reflecting ν₀)
                                     (ι-is-embedding ν₀)
                                      _  ι-is-order-reflecting ν₁)
ι-is-order-reflecting (⌜Σ⌝ ν A)  = pair-fun-is-order-reflecting
                                    (Δ ν)
                                    (Κ ν)
                                    (Δ  A)
                                    (𝓚 ν A)
                                    (ι ν)
                                     x  γ x  ι (A x))
                                    (ι-is-order-reflecting ν)
                                    (ι-is-embedding ν)
  open Κ-extension ν A

  IH : (x :  Δ ν ) (y z :  Δ (A x) )
      ι (A x) y ≺⟨ Κ (A x)  ι (A x) z
              y ≺⟨ Δ (A x)          z
  IH x = ι-is-order-reflecting (A x)

  f : (x :  Δ ν ) (y z :  Δ (A x) )
     γ x (ι (A x) y) ≺⟨ 𝓚 ν A (ι ν x)  γ x (ι (A x) z)
     ι (A x) y       ≺⟨ Κ (A x)         ι (A x) z
  f x y z = inverses-of-order-equivs-are-order-reflecting [ 𝓚 ν A (ι ν x) ] [ Κ (A x) ]
             (≃ₒ-to-fun-is-order-equiv [ 𝓚 ν A (ι ν x) ] [ Κ (A x) ] (ϕ x)) _ _

  g : (x :  Δ ν ) (y z :  Δ (A x) )
     γ x (ι (A x) y) ≺⟨ 𝓚 ν A (ι ν x)  γ x (ι (A x) z)
     y               ≺⟨ Δ (A x)         z
  g x y z l = IH x y z (f x y z l)

ι-is-dense : (ν : E)  is-dense (ι ν)
ι-is-dense ⌜𝟙⌝         = id-is-dense
ι-is-dense ⌜ω+𝟙⌝       = ι𝟙-dense fe₀
ι-is-dense (ν₀ ⌜+⌝ ν₁) = pair-fun-dense
                          (dep-cases  _  ι ν₀)  _  ι ν₁))
                          (dep-cases  _  ι-is-dense ν₀)  _  ι-is-dense ν₁))
ι-is-dense (ν₀ ⌜×⌝ ν₁) = pair-fun-dense _ _
                          (ι-is-dense ν₀)
                           _  ι-is-dense ν₁)
ι-is-dense (⌜Σ⌝ ν A)   = pair-fun-dense
                          (ι ν)
                           x  γ x  ι (A x))
                          (ι-is-dense ν)
                           x  comp-is-dense
                                  (ι-is-dense (A x))
                                    (γ x)
                                    (γ-is-equiv x)))
  open Κ-extension ν A


We define limit points as follows:


 recall-notion-of-isolatedness  : {X : 𝓤 ̇ } (x : X)
                                 is-isolated x  ((y : X)  is-decidable (x  y))
 recall-notion-of-isolatedness x = refl

is-limit-point : {X : 𝓤 ̇ }  X  𝓤 ̇
is-limit-point x = is-isolated x  WLPO


The characteristic function of limit points:


 : (ν : E)   Δ ν   𝟚
 ⌜𝟙⌝                     = 
 ⌜ω+𝟙⌝       (inl n)      = 
 ⌜ω+𝟙⌝       (inr )      = 
 (ν₀ ⌜+⌝ ν₁) (inl  , x₀) =  ν₀ x₀
 (ν₀ ⌜+⌝ ν₁) (inr  , x₁) =  ν₁ x₁
 (ν₀ ⌜×⌝ ν₁) (x₀ , x₁)    = max𝟚 ( ν₀ x₀) ( ν₁ x₁)
 (⌜Σ⌝ ν A)   (x  , y)     = max𝟚 ( ν x) ( (A x) y)


Non-limit points are isolated in the Κ interpretation:


ℓ-isolated : (ν : E) (x :  Δ ν )   ν x    is-isolated (ι ν x)
ℓ-isolated ⌜𝟙⌝                     p    = 𝟙-is-discrete 
ℓ-isolated ⌜ω+𝟙⌝       (inl n)      refl = finite-isolated fe₀ n
ℓ-isolated (ν₀ ⌜+⌝ ν₁) (inl  , x₀) p    = Σ-isolated
                                            (inl-is-isolated  (𝟙-is-discrete ))
                                            (ℓ-isolated ν₀ x₀ p)
ℓ-isolated (ν₀ ⌜+⌝ ν₁) (inr  , x₁) p    = Σ-isolated
                                            (inr-is-isolated  (𝟙-is-discrete ))
                                            (ℓ-isolated ν₁ x₁ p)
ℓ-isolated (ν₀ ⌜×⌝ ν₁) (x₀ , x₁)    p    = Σ-isolated
                                            (ℓ-isolated ν₀ x₀ (max𝟚-₀-left p))
                                            (ℓ-isolated ν₁ x₁ (max𝟚-₀-right p))
ℓ-isolated (⌜Σ⌝ ν A)   (x , y)      p    = iv
  open Κ-extension ν A

  i : is-isolated (ι ν x)
  i = ℓ-isolated ν x (max𝟚-₀-left p)

  ii : is-isolated (ι (A x) y)
  ii = ℓ-isolated (A x) y (max𝟚-₀-right p)

  iii : is-isolated (γ x (ι (A x) y))
  iii = equivs-preserve-isolatedness (γ x) (γ-is-equiv x) (ι (A x) y) ii

  iv : is-isolated (ι ν x , γ x (ι (A x) y))
  iv = Σ-isolated i iii


The function ℓ really does detect limit points:


module _ (pe : propext 𝓤₀) where

 ℓ-limit : (ν : E) (x :  Δ ν )   ν x    is-limit-point (ι ν x)
 ℓ-limit ⌜ω+𝟙⌝       (inr )      p i = is-isolated-gives-is-isolated'  i
 ℓ-limit (ν₀ ⌜+⌝ ν₁) (inl  , x₀) p i = ℓ-limit ν₀ x₀ p
                                           (underlying-type-is-setᵀ fe 𝟚ᵒ) i)
 ℓ-limit (ν₀ ⌜+⌝ ν₁) (inr  , x₁) p i = ℓ-limit ν₁ x₁ p
                                           (underlying-type-is-setᵀ fe 𝟚ᵒ) i)
 ℓ-limit (ν₀ ⌜×⌝ ν₁) (x₀ , x₁)    p i =
   Cases (max𝟚-lemma p)
     (p₀ :  ν₀ x₀  )  ℓ-limit ν₀ x₀ p₀ (×-isolated-left i))
     (p₁ :  ν₁ x₁  )  ℓ-limit ν₁ x₁ p₁ (×-isolated-right i))
 ℓ-limit (⌜Σ⌝ ν A)   (x , y)      p i =
   Cases (max𝟚-lemma p)
     (p₀ :  ν x  )
            ℓ-limit ν x p₀ (Σ-isolated-left (𝓚-Compact pe ν A) i))
     (p₁ :  (A x) y  )
            ℓ-limit (A x) y p₁
              (equivs-reflect-isolatedness (γ x)
                (γ-is-equiv x)
                (ι (A x) y)
                  (underlying-type-is-setᵀ fe (Κ ν)) i)))
   open Κ-extension ν A

 isolatedness-decision : (ν : E) (x :  Δ ν )
                        is-isolated (ι ν x) + is-limit-point (ι ν x)
 isolatedness-decision ν x = 𝟚-equality-cases
                               (p :  ν x  )  inl (ℓ-isolated ν x p))
                               (p :  ν x  )  inr (ℓ-limit ν x p))

 isolatedness-decision' : ¬ WLPO
                         (ν : E) (x :  Δ ν )
                         is-decidable (is-isolated (ι ν x))
 isolatedness-decision' f ν x =
   Cases (isolatedness-decision ν x)
     (g : is-isolated (ι ν x)  WLPO)   inr (contrapositive g f))


We conclude with some impossibility results.


ι-is-equiv-gives-LPO : ((ν : E)  is-equiv (ι ν))
ι-is-equiv-gives-LPO f = ι𝟙-is-equiv-gives-LPO (f ⌜ω+𝟙⌝)

LPO-gives-ι-is-equiv : LPO
                      (ν : E)  is-equiv (ι ν)
LPO-gives-ι-is-equiv lpo ⌜𝟙⌝         = id-is-equiv 𝟙
LPO-gives-ι-is-equiv lpo ⌜ω+𝟙⌝       = LPO-gives-ι𝟙-is-equiv lpo
LPO-gives-ι-is-equiv lpo (ν₀ ⌜+⌝ ν₁) = pair-fun-is-equiv
                                          (dep-cases  _  ι ν₀)  _  ι ν₁))
                                          (id-is-equiv (𝟙 + 𝟙))
                                             _  LPO-gives-ι-is-equiv lpo ν₀)
                                             _  LPO-gives-ι-is-equiv lpo ν₁))
LPO-gives-ι-is-equiv lpo (ν₀ ⌜×⌝ ν₁) = pair-fun-is-equiv _ _
                                          (LPO-gives-ι-is-equiv lpo ν₀)
                                           _  LPO-gives-ι-is-equiv lpo ν₁)
LPO-gives-ι-is-equiv lpo (⌜Σ⌝ ν A)   = pair-fun-is-equiv
                                          (ι ν)
                                           x  γ x  ι (A x))
                                          (LPO-gives-ι-is-equiv lpo ν)
                                           x  ∘-is-equiv
                                                  (LPO-gives-ι-is-equiv lpo (A x))
                                                  (γ-is-equiv x))
  open Κ-extension ν A

ι-is-equiv-iff-LPO : ((ν : E)  is-equiv (ι ν))  LPO
ι-is-equiv-iff-LPO = ι-is-equiv-gives-LPO , LPO-gives-ι-is-equiv


We also have the following:


ι-has-section-gives-Κ-discrete : (ν : E)  has-section (ι ν)  is-discrete  Κ ν 
ι-has-section-gives-Κ-discrete ν (θ , ιθ) = lc-maps-reflect-discreteness θ
                                              (sections-are-lc θ (ι ν , ιθ))
                                              (Δ-is-discrete ν)

ι-is-equiv-gives-Κ-discrete : (ν : E)  is-equiv (ι ν)  is-discrete  Κ ν 
ι-is-equiv-gives-Κ-discrete ν e = ι-has-section-gives-Κ-discrete ν
                                   (equivs-have-sections (ι ν) e)

LPO-gives-Κ-discrete : LPO
                      (ν : E)  is-discrete  Κ ν 
LPO-gives-Κ-discrete lpo ν = ι-is-equiv-gives-Κ-discrete ν
                              (LPO-gives-ι-is-equiv lpo ν)

Κ-discrete-gives-WLPO : ((ν : E)  is-discrete  Κ ν )
Κ-discrete-gives-WLPO f = ℕ∞-discrete-gives-WLPO (f ⌜ω+𝟙⌝)


TODO. Can we close the gap between the last two facts? The difficulty
that arises here is similar to the following.

Let P be a proposition and assume function extensionality.

(0) If P is decidable, then the function type (P → 𝟚) has decidable equality.

(1) If (P → 𝟚) has decidable equality, then ¬ P is decidable.

It doesn't seem to be possible to reverse any of the implications (0)
and (1), so that the proposition "(P -> 2) has decidable equality"
seems to be strictly between "P is decidable" and "¬P is decidable".

This is discussed in the file Taboos.P2.

TODO. Do we have (ν : E) → [ Δ ν ] ⊴ [ Κ ν ]? Notice that we do have
(ω +ₒ 𝟙ₒ) ⊴ ℕ∞ₒ, proved in OrdinalOfOrdinals, submodule ℕ∞-in-Ord.

TODO. Define an element x of an ordinal to be trisolated if for every
y we have that y ≺ x or x = y or x ≺ y.  Notice that trisolated
elements are isolated. Define an ordinal to be trichotomous if every
element is trisolated. (1) Δ ν should be trichotomous. (2) We should have:

ℓ-trisolated : (ν : E) (x : ⟨ Δ ν ⟩) → ℓ ν x = ₀ → is-trisolated (ι ν x)

We don't need to discuss the case ℓ ν x = ₁ because this is already
covered by ℓ-limit as trisolated points are isolated.

TODO. An element x of α is trisolated iff there are ordinals αₕ and αₜ
and an ordinal-equivalence αₕ +ₒ 𝟙ₒ + αₜ → α that maps the point at
the component 𝟙ₒ to x.

TODO. Suprema of compact ordinals are compact. (This follows directly
from the constructions in the file OrdinalOfOrdinalsSupremum.)