Tom de Jong, 1 and 4 April 2022.

\begin{code}

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

module Ordinals.Taboos where

open import MLTT.Plus-Properties
open import MLTT.Spartan hiding (๐Ÿš ; โ‚€ ; โ‚)
open import Ordinals.Equivalence
open import Ordinals.Maps
open import Ordinals.Notions
open import Ordinals.Type
open import Ordinals.Underlying
open import UF.DiscreteAndSeparated hiding (๐Ÿš-is-discrete)
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.ClassicalLogic
open import UF.FunExt
open import UF.PropTrunc
open import UF.Size
open import UF.Subsingletons
open import UF.UA-FunExt
open import UF.Univalence

\end{code}

We show that two classically true statements about ordinals are constructively
unacceptable, because each of them implies excluded middle.

The first statement is that every discrete ordinal is trichotomous. Classically,
this is trivial, because every ordinal is trichotomous (and discrete).
Constructively, the converse (trichotomous implies discrete) *does* hold.

The second statement is that the supremum of a family of trichotomous ordinals
indexed by a discrete type is again discrete.

\begin{code}

Every-Discrete-Ordinal-Is-Trichotomous : (๐“ค : Universe) โ†’ ๐“ค โบ ฬ‡
Every-Discrete-Ordinal-Is-Trichotomous ๐“ค =
 ((ฮฑ : Ordinal ๐“ค) โ†’ is-discrete โŸจ ฮฑ โŸฉ
                  โ†’ is-trichotomous-order (underlying-order ฮฑ))

module suprema-of-ordinals-assumptions
        (pt : propositional-truncations-exist)
        (sr : Set-Replacement pt)
        (ua : Univalence)
       where

 open import Ordinals.OrdinalOfOrdinalsSuprema ua
 open suprema pt sr public

 Sups-Of-Discretely-Indexed-Trichotomous-Ordinals-Are-Discrete :
  (๐“ค : Universe) โ†’ ๐“ค โบ ฬ‡
 Sups-Of-Discretely-Indexed-Trichotomous-Ordinals-Are-Discrete ๐“ค =
  (I : ๐“ค ฬ‡ ) โ†’ is-discrete I โ†’ (ฮฑ : I โ†’ Ordinal ๐“ค)
             โ†’ ((i : I) โ†’ is-trichotomous-order (underlying-order (ฮฑ i)))
             โ†’ is-discrete โŸจ sup ฮฑ โŸฉ

\end{code}

In showing that the first statement implies excluded middle, the two-element
type in some fixed but arbitrary universe ๐“ค will be useful.

\begin{code}

module _ {๐“ค : Universe} where

 ๐Ÿš : ๐“ค ฬ‡
 ๐Ÿš = ๐Ÿ™ {๐“ค} + ๐Ÿ™ {๐“ค}

 pattern โ‚€ = inl โ‹†
 pattern โ‚ = inr โ‹†

 ๐Ÿš-is-discrete : is-discrete ๐Ÿš
 ๐Ÿš-is-discrete = +-is-discrete ๐Ÿ™-is-discrete ๐Ÿ™-is-discrete

\end{code}

We now work towards proving that excluded middle follows from the assertion that
every discrete ordinal is trichotomous.

The outline of the proof is given here:
(1) Fix a type P and construct a transitive and well-founded relation โ‰บ on ๐Ÿš
    involving P.
(2) If P is a proposition, then โ‰บ is prop-valued.
(3) If ยฌยฌ P holds, then โ‰บ is extensional.
(4) Hence, if P is a proposition such that ยฌยฌ P holds, then (๐Ÿš , โ‰บ) is a
    (discrete) ordinal.
(5) The order โ‰บ is trichotomous if and only if P holds.

Hence, if every discrete ordinal is trichotomous, then ยฌยฌ P โ†’ P for every
proposition P, which is equivalent to excluded middle.

\begin{code}

module discrete-trichotomous-taboo-construction
        (P : ๐“ค ฬ‡ )
       where

 _โ‰บ_ : ๐Ÿš {๐“ค} โ†’ ๐Ÿš {๐“ค} โ†’ ๐“ค ฬ‡
 โ‚€ โ‰บ โ‚€ = ๐Ÿ˜
 โ‚€ โ‰บ โ‚ = P
 โ‚ โ‰บ โ‚€ = ๐Ÿ˜
 โ‚ โ‰บ โ‚ = ๐Ÿ˜

 โ‰บ-is-prop-valued : is-prop P โ†’ is-prop-valued _โ‰บ_
 โ‰บ-is-prop-valued i โ‚€ โ‚€ = ๐Ÿ˜-is-prop
 โ‰บ-is-prop-valued i โ‚€ โ‚ = i
 โ‰บ-is-prop-valued i โ‚ โ‚€ = ๐Ÿ˜-is-prop
 โ‰บ-is-prop-valued i โ‚ โ‚ = ๐Ÿ˜-is-prop

 โ‰บ-is-transitive : transitive _โ‰บ_
 โ‰บ-is-transitive โ‚€ โ‚ โ‚€ u v = v
 โ‰บ-is-transitive โ‚€ โ‚ โ‚ u v = u
 โ‰บ-is-transitive โ‚ โ‚€ z u v = ๐Ÿ˜-elim u
 โ‰บ-is-transitive โ‚ โ‚ z u v = ๐Ÿ˜-elim u

 โ‰บ-well-founded-lemma : (y : ๐Ÿš) โ†’ y โ‰บ โ‚€ โ†’ is-accessible _โ‰บ_ y
 โ‰บ-well-founded-lemma โ‚€ l = ๐Ÿ˜-elim l
 โ‰บ-well-founded-lemma โ‚ l = ๐Ÿ˜-elim l

 โ‰บ-is-well-founded : is-well-founded _โ‰บ_
 โ‰บ-is-well-founded โ‚€ = acc โ‰บ-well-founded-lemma
 โ‰บ-is-well-founded โ‚ = acc ฮณ
  where
   ฮณ : (y : ๐Ÿš) โ†’ y โ‰บ โ‚ โ†’ is-accessible _โ‰บ_ y
   ฮณ โ‚€ l = acc โ‰บ-well-founded-lemma

 โ‰บ-is-extensional : ยฌยฌ P โ†’ is-extensional _โ‰บ_
 โ‰บ-is-extensional h โ‚€ โ‚€ u v = refl
 โ‰บ-is-extensional h โ‚ โ‚ u v = refl
 โ‰บ-is-extensional h โ‚€ โ‚ u v = ๐Ÿ˜-elim (h ฮณ)
  where
   ฮณ : ยฌ P
   ฮณ p = ๐Ÿ˜-elim (v โ‚€ p)
 โ‰บ-is-extensional h โ‚ โ‚€ u v = ๐Ÿ˜-elim (h ฮณ)
  where
   ฮณ : ยฌ P
   ฮณ p = ๐Ÿ˜-elim (u โ‚€ p)

 ๐Ÿšโ‰บ-ordinal : is-prop P โ†’ ยฌยฌ P โ†’ Ordinal ๐“ค
 ๐Ÿšโ‰บ-ordinal i h = ๐Ÿš , _โ‰บ_ , โ‰บ-is-prop-valued i   , โ‰บ-is-well-founded
                          , โ‰บ-is-extensional h , โ‰บ-is-transitive

 โ‰บ-trichotomous-characterization : is-trichotomous-order _โ‰บ_ โ†” P
 โ‰บ-trichotomous-characterization = โฆ…โ‡’โฆ† , โฆ…โ‡โฆ†
  where
   โฆ…โ‡โฆ† : P โ†’ is-trichotomous-order _โ‰บ_
   โฆ…โ‡โฆ† p โ‚€ โ‚€ = inr (inl refl)
   โฆ…โ‡โฆ† p โ‚€ โ‚ = inl p
   โฆ…โ‡โฆ† p โ‚ โ‚€ = inr (inr p)
   โฆ…โ‡โฆ† p โ‚ โ‚ = inr (inl refl)
   โฆ…โ‡’โฆ† : is-trichotomous-order _โ‰บ_ โ†’ P
   โฆ…โ‡’โฆ† t = lemma (t โ‚€ โ‚)
    where
     lemma : (โ‚€ โ‰บ โ‚) + (โ‚€ ๏ผ โ‚) + (โ‚ โ‰บ โ‚€) โ†’ P
     lemma (inl p)       = p
     lemma (inr (inl e)) = ๐Ÿ˜-elim (+disjoint e)
     lemma (inr (inr l)) = ๐Ÿ˜-elim l

\end{code}

The above construction quickly yields the first promised result.

\begin{code}

DNE-if-Every-Discrete-Ordinal-Is-Trichotomous :
   Every-Discrete-Ordinal-Is-Trichotomous ๐“ค
 โ†’ DNE ๐“ค
DNE-if-Every-Discrete-Ordinal-Is-Trichotomous h P P-is-prop not-not-P =
 lr-implication โ‰บ-trichotomous-characterization
                  (h (๐Ÿšโ‰บ-ordinal P-is-prop not-not-P) (๐Ÿš-is-discrete))
  where
   open discrete-trichotomous-taboo-construction P

EM-if-Every-Discrete-Ordinal-Is-Trichotomous :
   funext ๐“ค ๐“คโ‚€
 โ†’ Every-Discrete-Ordinal-Is-Trichotomous ๐“ค
 โ†’ EM ๐“ค
EM-if-Every-Discrete-Ordinal-Is-Trichotomous fe h =
 DNE-gives-EM fe (DNE-if-Every-Discrete-Ordinal-Is-Trichotomous h)

\end{code}

It is somewhat more involved to get a taboo from the assertion that
discretely-indexed suprema of trichotomous ordinals are discrete.

The first step is fairly straightforward however and once again involves
constructing an ordinal that depends on a proposition P. What matters is that:
(1) the constructed ordinal is trichotomous;
(2) an initial segment of the ordinal is equivalent to P.

\begin{code}

module _
        (fe : FunExt)
       where

 open import Ordinals.Arithmetic fe
 open import Ordinals.WellOrderArithmetic

 module discrete-sup-taboo-construction-I
         (P : ๐“ค ฬ‡ )
         (P-is-prop : is-prop P)
        where

  P' : Ordinal ๐“ค
  P' = prop-ordinal P P-is-prop +โ‚’ ๐Ÿ™โ‚’

  P'-is-trichotomous : is-trichotomous-order (underlying-order P')
  P'-is-trichotomous = trichotomy-preservation (prop.trichotomous P P-is-prop)
                                               (prop.trichotomous ๐Ÿ™ ๐Ÿ™-is-prop)
   where
    open plus (prop.order P P-is-prop) (prop.order ๐Ÿ™ ๐Ÿ™-is-prop)

\end{code}

Next, we turn to the second part of our construction, which defines a
discretely-indexed family of trichotomous ordinals. To work with (suprema of)
ordinals, we need additional assumptions and imports.

\begin{code}

module _
        (pt : propositional-truncations-exist)
        (sr : Set-Replacement pt)
        (ua : Univalence)
       where

 open suprema-of-ordinals-assumptions pt sr ua

 private
  fe : FunExt
  fe = Univalence-gives-FunExt ua

 open import NotionsOfDecidability.Decidable
 open import NotionsOfDecidability.DecidableClassifier
 open import NotionsOfDecidability.Complemented

 open import Ordinals.Arithmetic fe
 open import Ordinals.OrdinalOfOrdinals ua
 open import Ordinals.WellOrderArithmetic

 open import UF.Embeddings
 open import UF.ImageAndSurjection pt

 module discrete-sup-taboo-construction-II
          (P : ๐“ค ฬ‡ )
          (P-is-prop : is-prop P)
         where

  open discrete-sup-taboo-construction-I fe P P-is-prop

  I : ๐“ค ฬ‡
  I = ๐Ÿš {๐“ค}

  ฮฑ : I โ†’ Ordinal ๐“ค
  ฮฑ โ‚€ = P'
  ฮฑ โ‚ = ๐Ÿ™โ‚’ +โ‚’ ๐Ÿ™โ‚’

  ฮฑ-is-trichotomous : (i : I) โ†’ is-trichotomous-order (underlying-order (ฮฑ i))
  ฮฑ-is-trichotomous โ‚€ = P'-is-trichotomous
  ฮฑ-is-trichotomous โ‚ = trichotomy-preservation trichotomous trichotomous
   where
    open prop ๐Ÿ™ ๐Ÿ™-is-prop
    open plus (underlying-order ๐Ÿ™โ‚’) (underlying-order ๐Ÿ™โ‚’)

\end{code}

We will derive decidability of P from the assumption that the supremum of ฮฑ is
discrete.

The idea of the proof is captured by NBโ‚ and NBโ‚‚ below. We will decide P by
deciding whether (ฮฑ โ‚€ โ†“ inr โ‹†) and (ฮฑ โ‚ โ†“ inr โ‹†) are equivalent ordinals.

This, in turn, is decidable, because both ordinals are images of an embedding
e : โŸจ sup ฮฑ โŸฉ โ†’ Ordinal ๐“ค and โŸจ sup ฮฑ โŸฉ is discrete by assumption.

\begin{code}

  fact-I : โŸจ ฮฑ โ‚€ โ†“ inr โ‹† โŸฉ โ†’ P
  fact-I (inl p , _) = p

  NBโ‚ : โŸจ ฮฑ โ‚€ โ†“ inr โ‹† โŸฉ โ‰ƒ P
  NBโ‚ = qinveq f (g , ฮท , ฮต)
   where
    f : โŸจ ฮฑ โ‚€ โ†“ โ‚ โŸฉ โ†’ P
    f = fact-I
    g : P โ†’ โŸจ ฮฑ โ‚€ โ†“ โ‚ โŸฉ
    g p = (inl p , โ‹†)
    ฮท : g โˆ˜ f โˆผ id
    ฮท (inl p , _) = to-subtype-๏ผ (ฮป x โ†’ Prop-valuedness P' x โ‚) refl
    ฮต : f โˆ˜ g โˆผ id
    ฮต p = P-is-prop (f (g p)) p

  NBโ‚‚ : โŸจ ฮฑ โ‚ โ†“ inr โ‹† โŸฉ โ‰ƒ ๐Ÿ™{๐“ค}
  NBโ‚‚ = singleton-โ‰ƒ-๐Ÿ™ (x , c)
   where
    x : โŸจ ฮฑ โ‚ โ†“ inr โ‹† โŸฉ
    x = (inl โ‹† , โ‹†)
    c : is-central (โŸจ ฮฑ โ‚ โ†“ inr โ‹† โŸฉ) (โ‚€ , โ‹†)
    c (inl โ‹† , โ‹†) = refl

  fact-II : P โ†’ (ฮฑ โ‚€ โ†“ inr โ‹†) โ‰ƒโ‚’ (ฮฑ โ‚ โ†“ inr โ‹†)
  fact-II p = f , (f-order-pres , f-is-equiv , g-order-pres)
   where
    f : โŸจ ฮฑ โ‚€ โ†“ inr โ‹† โŸฉ โ†’ โŸจ ฮฑ โ‚ โ†“ inr โ‹† โŸฉ
    f _ = inl โ‹† , โ‹†
    g : โŸจ ฮฑ โ‚ โ†“ inr โ‹† โŸฉ โ†’ โŸจ ฮฑ โ‚€ โ†“ inr โ‹† โŸฉ
    g _ = inl p , โ‹†
    f-order-pres : is-order-preserving (ฮฑ โ‚€ โ†“ inr โ‹†) (ฮฑ โ‚ โ†“ inr โ‹†) f
    f-order-pres (inl p , _) (inl q , _) l = ๐Ÿ˜-elim l
    g-order-pres : is-order-preserving (ฮฑ โ‚ โ†“ inr โ‹†) (ฮฑ โ‚€ โ†“ inr โ‹†) g
    g-order-pres (inl โ‹† , _) (inl โ‹† , _) l = ๐Ÿ˜-elim l
    f-is-equiv : is-equiv f
    f-is-equiv = qinvs-are-equivs f (g , ฮท , ฮต)
     where
      ฮต : f โˆ˜ g โˆผ id
      ฮต (inl โ‹† , _) = refl
      ฮท : g โˆ˜ f โˆผ id
      ฮท (inl q , _) = to-subtype-๏ผ (ฮป x โ†’ Prop-valuedness P' x โ‚)
                                   (ap inl (P-is-prop p q))

  fact-III : (ฮฑ โ‚€ โ†“ inr โ‹†) โ‰ƒโ‚’ (ฮฑ โ‚ โ†“ inr โ‹†) โ†’ P
  fact-III e = fact-I (โ‰ƒโ‚’-to-funโปยน (ฮฑ โ‚€ โ†“ inr โ‹†) (ฮฑ โ‚ โ†“ inr โ‹†) e (inl โ‹† , โ‹†))

  decidability-if-sup-of-ฮฑ-discrete : is-discrete โŸจ sup ฮฑ โŸฉ โ†’ is-decidable P
  decidability-if-sup-of-ฮฑ-discrete ฮด = decidable-โ†” (fact-III , fact-II) dec
   where
    r : image (sum-to-ordinals ฮฑ) โ†’ Ordinal ๐“ค
    r = restriction (sum-to-ordinals ฮฑ)
    c : (ฮฃ i ๊ž‰ I , โŸจ ฮฑ i โŸฉ) โ†’ image (sum-to-ordinals ฮฑ)
    c = corestriction (sum-to-ordinals ฮฑ)

    ฯ† : โŸจ sup ฮฑ โŸฉ โ‰ƒ image (sum-to-ordinals ฮฑ)
    ฯ† = sup-is-image-of-sum-to-ordinals ฮฑ
    f : (ฮฃ i ๊ž‰ I , โŸจ ฮฑ i โŸฉ) โ†’ โŸจ sup ฮฑ โŸฉ
    f = โŒœ ฯ† โŒโปยน โˆ˜ c
    e : โŸจ sup ฮฑ โŸฉ โ†’ Ordinal ๐“ค
    e = r โˆ˜ โŒœ ฯ† โŒ

    e-is-embedding : is-embedding e
    e-is-embedding =
     โˆ˜-is-embedding (equivs-are-embeddings โŒœ ฯ† โŒ (โŒœโŒ-is-equiv ฯ†))
                    (restrictions-are-embeddings (sum-to-ordinals ฮฑ))
    e-after-f-lemma : e โˆ˜ f โˆผ sum-to-ordinals ฮฑ
    e-after-f-lemma (i , x) =
     (r โˆ˜ โŒœ ฯ† โŒ โˆ˜ โŒœ ฯ† โŒโปยน โˆ˜ c) (i , x) ๏ผโŸจ h    โŸฉ
     r (c (i , x))                     ๏ผโŸจ refl โŸฉ
     sum-to-ordinals ฮฑ (i , x)         โˆŽ
      where
       h = ap r (inverses-are-sections โŒœ ฯ† โŒ (โŒœโŒ-is-equiv ฯ†) (c (i , x)))

    dec : is-decidable ((ฮฑ โ‚€ โ†“ inr โ‹†) โ‰ƒโ‚’ (ฮฑ โ‚ โ†“ inr โ‹†))
    dec = decidable-cong ฮณ (ฮด (f (โ‚€ , inr โ‹†)) (f (โ‚ , inr โ‹†)))
     where
      ฮณ = (f (โ‚€ , inr โ‹†)     ๏ผ  f (โ‚ , inr โ‹†))     โ‰ƒโŸจ โฆ…1โฆ† โŸฉ
          (e (f (โ‚€ , inr โ‹†)) ๏ผ  e (f (โ‚ , inr โ‹†))) โ‰ƒโŸจ โฆ…2โฆ† โŸฉ
          ((ฮฑ โ‚€ โ†“ inr โ‹†)     ๏ผ  (ฮฑ โ‚ โ†“ inr โ‹†))     โ‰ƒโŸจ โฆ…3โฆ† โŸฉ
          ((ฮฑ โ‚€ โ†“ inr โ‹†)     โ‰ƒโ‚’ (ฮฑ โ‚ โ†“ inr โ‹†))     โ– 
       where
        โฆ…1โฆ† = โ‰ƒ-sym (embedding-criterion-converse e e-is-embedding
                      (f (โ‚€ , inr โ‹†)) (f (โ‚ , inr โ‹†)))
        โฆ…2โฆ† = ๏ผ-cong _ _ (e-after-f-lemma (โ‚€ , inr โ‹†))
                         (e-after-f-lemma (โ‚ , inr โ‹†))
        โฆ…3โฆ† = UAโ‚’-โ‰ƒ (ua ๐“ค) (fe _ _) (ฮฑ โ‚€ โ†“ inr โ‹†) (ฮฑ โ‚ โ†“ inr โ‹†)

\end{code}

Finally, we derive excluded middle from the assumption that discretely-indexed
suprema of trichotomous ordinals are discrete, as announced at the top of this
file.

\begin{code}

 EM-if-Sups-Of-Discretely-Indexed-Trichotomous-Ordinals-Are-Discrete :
  Sups-Of-Discretely-Indexed-Trichotomous-Ordinals-Are-Discrete ๐“ค
  โ†’ EM ๐“ค
 EM-if-Sups-Of-Discretely-Indexed-Trichotomous-Ordinals-Are-Discrete h P i =
  decidability-if-sup-of-ฮฑ-discrete ฮณ
   where
    open discrete-sup-taboo-construction-II P i
    ฮณ : is-discrete โŸจ sup ฮฑ โŸฉ
    ฮณ = h ๐Ÿš ๐Ÿš-is-discrete ฮฑ ฮฑ-is-trichotomous

\end{code}