Martin Escardo, 4th October 2018

We worked with ordinals with top in order to be able to construct the
sum of an ordinal-indexed family of ordinals, with the lexicographic
order. Here we justify that some such restriction is needed.

This implements the following email communication:

On 22/07/18 06:17, Michael Shulman wrote:
> Ah, I see.  In fact I think "every subset of an ordinal is an
> ordinal" is equivalent to LEM as follows: consider the ordinal Prop,
> with (P < Q) = (~P /\ Q) as before, and consider the subset A of all
> P such that ~~P is true.  Then False \notin A, so given any Q \in A,
> we cannot have any P \in A with P < Q.  Thus the hypothesis of
> extensionality for A is vacuous, so to say that A is extensional is
> to say that it is a prop.  But True \in A, so this is to say
> that ~~P -> (P = True), i.e. DNE holds, hence LEM.
>
> On Fri, Jul 20, 2018 at 3:42 PM, Martin Escardo <m.escardo@cs.bham.ac.uk> wrote:
>> On 20/07/18 23:31, Michael Shulman wrote:
>>> Do you know of a model in which preservation of extensionality
>>> definitely fails (or a proof of a taboo from it)?
>>
>> No. But here is an idea that made me to give up trying to prove
>> extensionality of the lexicographic order on Sigma.
>>
>> Any prop is an ordinal in a unique way (with the empty order).
>>
>> Now suppose that X is an ordinal, and consider P:X->U prop
>> valued.  Then the lexicographic order on the sum Sigma (x:X),P (x) is
>> nothing but a subset of X. While classically the subset will remain
>> extensional (for if we have x and y not equal, then either x<y or
>> y<x, and hence they will not have the same lower set),
>> constructively this seems very dubious.

\begin{code}

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

open import MLTT.Spartan

open import UF.FunExt
open import UF.Subsingletons

module Ordinals.ShulmanTaboo
       (fe : FunExt)
       (pe : propext 𝓤₀)
       where

open import Ordinals.Type
open import Ordinals.OrdinalOfTruthValues fe 𝓤₀ pe
open import Ordinals.Notions
open import Ordinals.Underlying

open import UF.Base
open import UF.ClassicalLogic
open import UF.SubtypeClassifier
open import UF.Subsingletons-FunExt

fe₀ : funext 𝓤₀ 𝓤₀
fe₀ = fe 𝓤₀ 𝓤₀

\end{code}

The type of truth values is Ω, following topos-theoretic notation, and
the ordinal of truth values, ordered by p < q iff p ＝ ⊥ and q ＝ ⊤, is
denoted by Ωₒ (the subscript is the letter "o", for "ordinal", and not
the number zero). This is parametrized by an arbitrary universe, which
in this module is instantiated to 𝓤₀.

\begin{code}

X : 𝓤₁ ̇
X = Σ p ꞉ ⟨ Ωₒ ⟩ , ¬ (p ＝ ⊥)

recall-that : is-extensional (underlying-order Ωₒ)
recall-that = Extensionality Ωₒ

\end{code}

However, the extensionality of the restriction of the underlying order
of the ordinal Ωₒ of truth values to X is a constructive taboo (it
implies excluded middle), as shown by Shulman in the message quoted
above:

\begin{code}

_≺_ : X → X → 𝓤₁ ̇
(p , _) ≺ (q , _) = p ≺⟨ Ωₒ ⟩ q

shulmans-taboo : is-extensional _≺_ → EM 𝓤₀
shulmans-taboo e = DNE-gives-EM fe₀ δ
 where
  i : is-prop X
  i x y = e x y f g
   where
    f : (z : X) → z ≺ x → z ≺ y
    f (p , φ) (a , _) = 𝟘-elim (φ a)

    g : (z : X) → z ≺ y → z ≺ x
    g (q , ψ) (b , _) = 𝟘-elim (ψ b)

  δ : (P : 𝓤₀ ̇ ) → is-prop P → ¬¬ P → P
  δ P j φ = Idtofun s φ
   where
    p q : X
    p = (¬¬ P , negations-are-props fe₀) ,
        (λ r → Idtofun (ap pr₁ r) φ)
    q = (P , j) ,
        (λ r → φ (Idtofun (ap pr₁ r)))

    r : p ＝ q
    r = i p q

    s : ¬¬ P ＝ P
    s = ap (pr₁ ∘ pr₁) r

\end{code}

TODO: Use this to show that if the sum of any ordinal-indexed family
of ordinals is an ordinal under the lexicographic ordering, then
excluded middle holds, as explained in the message quoted
above. (Routine, tedious.)