----------------------------------------------------------------------------------------------------
-- Index of the Formalized Proofs in the paper
--
--     Type-Theoretic Approaches to Ordinals
--
--         Nicolai Kraus, Fredrik Nordvall-Forsberg, and Chuangjie Xu
----------------------------------------------------------------------------------------------------

-- We haven't proved in Agda all the statements about extensional wellfounded orders.
-- They are thus commented out in the following formulation of the theorems/lemmas.

-- Source files can be found at
--
--   https://bitbucket.org/nicolaikraus/constructive-ordinals-in-hott/
--
-- See `README.md` for versions of Agda and the cubical library that these
-- files are tested with.

{-# OPTIONS --cubical #-}

module index where

-- The following module gives an overview of the entire development
import Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Function
open import Cubical.Data.Empty
open import Cubical.Data.Sum
open import Cubical.Data.Sigma
open import Cubical.Data.Bool renaming (true to tt ; false to ff)
open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order as N hiding (_≟_ ; _>_)
open import Cubical.Relation.Nullary
open import Cubical.Relation.Binary
open BinaryRelation
open import Cubical.Induction.WellFounded
  renaming (WellFounded to isWellFounded)

open import PropTrunc

open import Iff
open import General-Properties
open import CantorNormalForm.Everything as C
open import BrouwerTree.Everything as B
open import ExtensionalWellfoundedOrder.Everything as O
open import Interpretations.CnfToBrw
open import Interpretations.CnfToBrw.Properties
open import Interpretations.BrwToOrd

import Abstract.Arithmetic


{- §2. Preliminaries -}

Lemma-1 : LPO ↔ WLPO × MP
Lemma-1 = (λ lpo → LPO→WLPO lpo , LPO→MP lpo) ,
          (λ (wlpo , mp) → WLPO×MP→LPO wlpo mp)

Lemma-2 : ((s : ℕ → Bool) → ∥ Σ[ n ∈ ℕ ] (s n ≡ tt) ∥ → Σ[ n ∈ ℕ ] (s n ≡ tt))
        × (LPO → (s : ℕ → Bool) → (∀ k → s k ≡ ff) ⊎ (Σ[ n ∈ ℕ ] (s n ≡ tt)))
Lemma-2 = (λ s → least-witness (λ z → s z ≡ tt) (λ _ → isSetBool _ _) (λ n → s n ≟ tt))
        , LPO-to-Σ-LPO


{- §4. An Abstract Axiomatic Framework for Ordinals -}

module _ {ℓ ℓ'} {A : Type ℓ}
  (_<_ _≤_   : A → A → Type ℓ')
  (A-is-set  : isSet A)
  (isProp⟨<⟩ : isPropValued _<_)
  (isProp⟨≤⟩ : isPropValued _≤_)
  (<-irrefl  : isIrrefl _<_)
  (<-trans   : isTrans _<_)
  (≤-refl    : isRefl _≤_)
  (≤-trans   : isTrans _≤_)
  (≤-antisym : isAntisym _≤_)
  (<-in-≤    : {a b : A} → a < b → a ≤ b)
  (<∘≤-in-<  : {a b c : A} → a < b → b ≤ c → a < c) where

 Lemma-3 : ∀ {ℓ''} {P : A → Type ℓ''}
         → isWellFounded _<_
         → (∀ a → (∀ b → b < a → P b) → P a)
         → ∀ a → P a
 Lemma-3 wf = WFI.induction wf

 Lemma-4 : isWellFounded _<_
         → (¬ (Σ[ f ∈ (ℕ → A) ] (∀ i → f (suc i) < f i)))
         × isIrrefl _<_
 Lemma-4 wf = no-infinite-descending-sequence wf , wellfounded→irreflexive wf

 Lemma-5 : (isIrrefl _<_ → ∀ {x y} → isProp ((x < y) ⊎ (x ≡ y)))
         × (isWellFounded _<_ → ∀ {x y} → isProp ((x < y) ⊎ (x ≡ y)))
 Lemma-5 = irreflexive→reflexive-closure-is-prop A-is-set isProp⟨<⟩
         , wellfounded→reflexive-closure-is-prop A-is-set isProp⟨<⟩

 open import Abstract.ZerSucLim _<_ _≤_ as A
 module AP = A.Properties A-is-set isProp⟨<⟩ isProp⟨≤⟩
                          <-irrefl ≤-refl ≤-trans ≤-antisym
                          <-in-≤ <∘≤-in-<

 Lemma-6 : (s : A → A) →
           (A.calc-suc s) ↔ (∀ b x → ((b < x) ↔ (s b ≤ x)))
 Lemma-6 = AP.calc-suc↔≤-<-characterization

 Remark-7 : (a : A) →
            ∥ Σ[ X ∈ Type ] (Σ[ f ∈ (X → A) ]
              ∥ X ∥ × ((x : X) → f x < a) × a A.is- X -sup-of f) ∥ → A.is-general-lim a
 Remark-7 a = ∥-∥rec (AP.isProp⟨is-general-lim⟩ a)
                    (λ (X , f , ∥X∥ , f<a , a-sup) →
                      AP.is-general-lim-some-family→is-general-lim  a X f ∥X∥ a-sup f<a)

 Lemma-8 : (a : A) → isProp (A.is-zero a ⊎ (A.is-strong-suc a ⊎ A.is-general-lim a))
                   × isProp (A.is-zero a ⊎ (A.is-strong-suc a ⊎ A.is-lim a))
 Lemma-8 a = (AP.isProp⟨is-weakly-classifiable⟩ a ,
              AP.isProp⟨is-classifiable⟩ a)

 Definition-9 : ∀ {ℓ''} → Type _
 Definition-9 {ℓ''} = A.satisfies-classifiability-induction ℓ''

 Corollary-10 : A.satisfies-classifiability-induction _ → A.has-classification
 Corollary-10 = AP.classifiability-induction→has-classification

 Theorem-11 :  A.has-classification → isWellFounded _<_
            → ∀ ℓ'' → A.satisfies-classifiability-induction ℓ''
 Theorem-11 cl wf ℓ'' = AP.ClassifiabilityInduction.ind cl wf {ℓ''}

 Definition-12 : Type _
 Definition-12 = Abstract.Arithmetic.has-unique-add _<_ _≤_

 Definition-13 : Type _
 Definition-13 = ∀ has-add →
   Abstract.Arithmetic.Multiplication.has-unique-mul _<_ _≤_ has-add

 Definition-14 : Type _
 Definition-14 = ∀ has-add has-mul →
   Abstract.Arithmetic.Exponentiation.has-unique-exp _<_ _≤_ has-add has-mul

 Definition-15 : Type _
 Definition-15 = ∀ has-add →
   Abstract.Arithmetic.Subtraction.has-unique-sub _<_ _≤_ has-add

 Lemma-16 : isIrrefl _<_ → isTrans _<_ → isTrichotomous _<_
          → ({a b c : A} → a < b → b ≤ c → a < c) ↔ Splits A _<_ _≤_
 Lemma-16 irrefl trans tri = <∘≤-in-<→Splits-≤ irrefl tri , Splits-≤→<∘≤-in-< trans

 Theorem-17 : A.has-zero → A.has-suc → A.has-limits
            → Discrete A → WLPO
 Theorem-17 A-has-zero A-has-suc A-has-lim = no-go-theorem
  where
   open A.no-go <-irrefl <-trans ≤-antisym <∘≤-in-< A-has-zero A-has-suc A-has-lim


{- §5. Cantor Normal Forms -}

Theorem-18 : isSet Cnf × isPropValued C._<_ × isPropValued C._≤_
           × isDecidable _≡_ × isDecidable C._<_ × isDecidable C._≤_
           × isTrans C._<_ × isExtensional C._<_
           × isTrans C._≤_ × isExtensional C._≤_
           × isIrrefl C._<_ × isRefl C._≤_ × isAntisym C._≤_
           × isTrichotomous C._<_ × isConnex C._≤_ × Splits Cnf C._<_ C._≤_
           × (∀{a b c} → a C.≤ b → b C.< c → a C.< c)
Theorem-18 = Cnf-is-set , (λ _ _ → C.isProp⟨<⟩) , (λ _ _ → C.isProp⟨≤⟩)
           , Cnf-is-discrete , C.<-dec , C.≤-dec
           , (λ _ _ _ → C.<-trans) , C.<-extensional
           , (λ _ _ _ → C.≤-trans) , C.≤-extensional
           , (λ _ → C.<-irrefl) , (λ _ → C.≤-refl) , (λ _ _ → C.≤-antisym)
           , C.<-tri , C.≤-connex , C.≤-splits
           , C.≤∘<-in-<

Theorem-19 : isWellFounded C._<_
Theorem-19 = C.<-is-wellfounded

Definition-20 : (Cnf → Cnf → Cnf) × (Cnf → Cnf → Cnf)
Definition-20 = C._+_ , C._·_

Lemma-21 : isAssoc C._+_ × (∀ x y z → y C.< z → x C.+ y C.< x C.+ z)
         × isAssoc C._·_ × (∀ x y z → x C.> C.𝟎 → y C.< z → x C.· y C.< x C.· z)
         × (∀ x y z → x C.· (y C.+ z) ≡ x C.· y C.+ x C.· z)
Lemma-21 = C.+-is-assoc , +r-is-<-monotone
         , C.·-is-assoc , ω^·-is-<-monotone
         , ·-is-left-distributive

Lemma-22 : C.is-zero 𝟎
         × C.calc-strong-suc (λ x → x C.+ 𝟏)
         × C.is-<-monotone (λ x → x C.+ 𝟏)
         × C.is-≤-monotone (λ x → x C.+ 𝟏)
Lemma-22 = 𝟎-is-zero
         , +𝟏-calc-strong-suc
         , succ-is-<-monotone
         , succ-is-≤-monotone

Definition-23 : Cnf × (Cnf → Cnf)
Definition-23 = C.ω , C.ω^⟨_⟩

Lemma-24 : (∀ a b → a C.≤ b → Σ[ c ∈ Cnf ] a C.+ c ≡ b)
         × (∀ a b → b C.> 𝟎 → Σ[ c ∈ Cnf ] Σ[ d ∈ Cnf ] (a ≡ b C.· c C.+ d) × (d C.< b))
Lemma-24 = C.Thm[sub]
         , C.Thm[div]

Theorem-25 : C.has-add
           × C.has-mul
           × C.has-exp-with-base C.ω
Theorem-25 = (C._+_ , C.+-is-add)
           , (C._·_ , C.·-is-mul)
           , (C.ω^⟨_⟩ , ω^⟨⟩-is-exp-with-base-ω)

Lemma-26 : (a : Cnf) → a > 𝟎 → ¬ (C.is-strong-suc a) → C.is-Σlim a
Lemma-26 = C.fundamental-sequence

Theorem-27 : ∀ ℓ →
             C.has-classification
           × C.satisfies-classifiability-induction ℓ
Theorem-27 ℓ = Cnf-has-classification , Cnf-satisfies-classifiability-induction ℓ

Theorem-28 : C.has-unique-add
           × C.has-unique-mul
           × C.has-unique-exp-with-base C.ω
Theorem-28 = Cnf-has-unique-add
           , Cnf-has-unique-mul
           , Cnf-has-unique-exp-with-base-ω

Theorem-29 : (C.has-limits → ⊥)
           × (LEM → ∀ f b → (∀ i → f i C.≤ b) → Σ[ a ∈ Cnf ] a C.is-sup-of f)
           × ((∀ f b → (∀ i → f i C.< b) → C.is-<-increasing f → Σ[ a ∈ Cnf ] a C.is-sup-of f) → WLPO)
Theorem-29 = Cnf-does-not-have-limits
           , LEM-computes-sup
           , having-limits-implies-WLPO


{- §6. Brouwer Ordinal Trees -}

Lemma-30 : (∀ {x} → ¬ (zero ≡ B.succ x))
         × (∀ {f f↑} → ¬ (zero ≡ B.limit f {f↑}))
         × (∀ {x f f↑} → ¬ (B.succ x ≡ B.limit f {f↑}))
Lemma-30 = B.zero≠succ , zero≠lim , succ≠lim

Lemma-31 : ∀ {x y} → x B.≤ y ↔ B.succ x B.≤ B.succ y
Lemma-31 = ≤-succ-mono , ≤-succ-mono⁻¹

Lemma-32 : ∀ x f {f↑} → x B.< limit f {f↑} → ∥ Σ[ n ∈ ℕ ] x B.< f n ∥
Lemma-32 = B.below-limit-lemma

Lemma-33 : ∀ f {f↑} g {g↑} → (limit f {f↑} B.≤ limit g {g↑}) → f ≲ g
Lemma-33 = B.lim≤lim→weakly-bisimilar

Lemma-34 : (∀ f x {f↑} → limit f {f↑} B.≤ B.succ x → limit f {f↑} B.≤ x)
         × (∀ f x {f↑} → x B.< limit f {f↑} → B.succ x B.< limit f {f↑})
Lemma-34 = B.lim≤sx→lim≤x
         , x<lim→sx<lim

Theorem-35 : isWellFounded B._<_
Theorem-35 = B.<-is-wellfounded

Theorem-36 : isAntisym B._≤_
Theorem-36 = λ _ _ → B.≤-antisym

Corollary-37 : isSet Brw × isPropValued B._<_ × isPropValued B._≤_
             × isTrans B._<_ × isIrrefl B._<_
             × isTrans B._≤_ × isRefl B._≤_ × isAntisym B._≤_
             × (∀ {a b c} → a B.< b → b B.≤ c → a B.< c)
             × (∀ {a b c} → a B.≤ b → b B.< c → a B.< c)
Corollary-37 = Brw-is-set , (λ _ _ → B.isProp⟨<⟩) , (λ _ _ → B.isProp⟨≤⟩)
             , B.<-trans , B.<-irreflexive
             , (λ _ _ _ → B.≤-trans) , (λ _ → B.≤-refl) , (λ _ _ → B.≤-antisym)
             , B.<∘≤-in-<
             , B.≤∘<-in-<

Theorem-38 : isExtensional B._<_ × isExtensional B._≤_
Theorem-38 = B.<-extensional , B.≤-extensional

Lemma-39 : B.has-zero × B.has-strong-suc × B.has-limits
Lemma-39 = (B.zero , B.zero-is-zero)
         , (B.succ , B.succ-calc-strong-suc)
         , (λ (f , f↑) → limit f {f↑}) , (λ (f , f↑) → limit-is-sup f f↑)

Corollary-40 : B.is-<-monotone B.succ
             × B.is-≤-monotone B.succ
Corollary-40 = <-succ-mono , ≤-succ-mono

Theorem-41 : ∀ ℓ →
             B.has-classification
           × B.satisfies-classifiability-induction ℓ
Theorem-41 ℓ = Brw-has-classification , Brw-satisfies-classifiability-induction ℓ

Theorem-42 : B.has-unique-add × B.has-unique-mul × B.has-unique-exp
Theorem-42 = Brw-has-unique-add , Brw-has-unique-mul , Brw-has-unique-exp

Lemma-43-i : (∀ {x y} z → x B.≤ y → x B.+ z B.≤ y B.+ z)
           × (∀ {x y} z → x B.≤ y → x B.· z B.≤ y B.· z)
Lemma-43-i = B.+x-mono , B.·x-mono
--
Lemma-43-ii : ∀ x {y z} → x B.+ y ≡ x B.+ z → y ≡ z
Lemma-43-ii = B.+-leftCancel
--
Lemma-43-iii : isAssoc B._+_
             × isAssoc B._·_
             × (∀ {x y} z → x B.· y B.+ x B.· z ≡ x B.· (y B.+ z))
Lemma-43-iii = (λ _ _ → B.+-assoc)
             , (λ _ _ → B.·-assoc)
             , B.·-+-distributivity
--
Lemma-43-iv : ∀ x y z → x B.^ (y B.+ z) ≡ x B.^ y B.· x B.^ z
Lemma-43-iv = λ x y z → B.exp-homomorphism {x} {y} {z}

Lemma-44 : (∀ x a → a B.< ω^ x → a B.+ ω^ x ≡ ω^ x)
         × (∀ x {a b} → a B.< ω^ x → b B.< ω^ x → a B.+ b B.< ω^ x)
         × (∀ {x n} → zero B.< x → ι (suc n) B.· ω^ x ≡ ω^ x)
Lemma-44 = B.additive-principal-ω^
         , B.additive-principal-ω^-closure
         , ω^x-absorbs-finite

Theorem-45 : (B.has-unique-sub ↔ B.has-sub)
           × (B.has-sub ↔ LPO)
Theorem-45 = (fst , Brw-sub-is-unique)
           , (B.has-sub→LPO , B.LPO→has-sub)

Theorem-46 : (∀ x → Dec (B.isFinite x))
           × (∀ x n → Dec (ι n  ≡  x)) × (∀ x n → Dec (x  ≡  ι n))
           × (∀ x n → Dec (ι n B.< x)) × (∀ x n → Dec (x B.< ι n))
           × (∀ x n → Dec (ι n B.≤ x)) × (∀ x n → Dec (x B.≤ ι n))
Theorem-46 = decIsFinite
           , dec-n≡ , dec-≡n
           , dec-n< , dec-<n
           , dec-n≤ , dec-≤n

Lemma-47 : (s : ℕ → Bool)
         → limit[ s ]↑ B.≤ ω·2
         × (∥ Σ[ k ∈ ℕ ] (s k ≡ tt) ∥ → limit[ s ]↑ ≡ ω·2)
         × (limit[ s ]↑ ≡ ω·2 → B.ω B.< limit[ s ]↑)
         × (B.ω B.< limit[ s ]↑ → Σ[ k ∈ ℕ ] (s k ≡ tt))
Lemma-47 s = jumpSeq≤ω2 s
           , jumpSeq-translate-forth s
           , lim⟨jumpSeq⟩≡ω+ω→lim⟨jumpSeq⟩>ω s
           , jumpSeq>ω-translate-back s

Theorem-48 : (LPO                       → (∀ x y → Dec (  x B.≤ y)))
           × ((∀ x y → Dec (  x B.≤ y)) → (∀ x y → Dec (  x B.< y)))
           × ((∀ x y → Dec (  x B.< y)) → (∀ x   → Dec (B.ω B.< x)))
           × ((∀ x   → Dec (B.ω B.< x)) → LPO)
           × (LPO                       → (∀ x y → Dec (x ≡ y)))
           × ((∀ x y → Dec (x ≡ y))     → (∀ x   → Dec (x ≡ ω·2)))
           × ((∀ x   → Dec (x ≡ ω·2))   → LPO)
Theorem-48 = LPO→Dec≤
           , Dec≤→Dec<
           , Dec<→Decω<
           , Decω<→LPO
           , LPO→Dec≡
           , Dec≡→Dec≡ω·2
           , Dec≡ω·2→LPO

Theorem-49 : WLPO ↔ (∀ x → Dec (x ≡ B.ω))
Theorem-49 = WLPO→Dec≡ω , Dec≡ω→WLPO

Theorem-50 : ∀ n →  N.≤ n → (LPO ↔ (∀ x → Dec (x ≡ B.ω B.· ι n)))
Theorem-50 n 2≤n = ((λ lpo x → LPO→Dec≡ lpo x (B.ω B.· ι n)) , Dec≡ωn→LPO n 2≤n)

Theorem-51 : (∀ x → Stable (x ≡ B.ω))
           × (∀ n →  N.≤ n → (∀ x → Stable (x ≡ B.ω B.· ι n)) → MP)
Theorem-51 = stable≡ω
           , stable≡ω·⟨n+2⟩→MP

Lemma-52 : LPO → (x y : Brw) → ¬ (x B.≤ y) → y B.< x
Lemma-52 = LPO→¬≤→>

Theorem-53 : (LPO                    → isTrichotomous B._<_)
           × (isTrichotomous B._<_   → Splits Brw B._<_ B._≤_)
           × (Splits Brw B._<_ B._≤_ → LPO)
Theorem-53 = LPO→trichotomy
           , trichotomy→splitting-≤
           , splitting-≤-to-LPO

Theorem-54 : (Σ[ _⊔_ ∈ (Brw → ℕ → Brw) ] (∀ x n → (x ⊔ n) B.is-join-of x and (ι n)))
           × (Σ[ _⊔ω ∈ (Brw → Brw) ] (∀ x → (x ⊔ω) B.is-join-of x and B.ω))
Theorem-54 = (with-finite._⊔_ , with-finite.is-join)
           , (with-ω._⊔ω , with-ω.is-join)

Theorem-55 : (LPO → Σ[ _⊔ω+1 ∈ (Brw → Brw) ] (∀ x → (x ⊔ω+1) B.is-join-of x and B.succ B.ω))
           × ((_⊔ω+1 : Brw → Brw) → (∀ x → (x ⊔ω+1) B.is-join-of x and B.succ B.ω) → WLPO)
Theorem-55 = (λ lpo → with-ω+1.⊔ω+1 lpo , with-ω+1.LPO→⊔ω+1 lpo)
           , (λ _⊔ω+1 p → Dec≡ω→WLPO (with-ω+1.⊔ω+1→Dec≡ω _⊔ω+1 p))

-- §6.7 An Alternative Definition of Brouwer Trees

import BrouwerTree.AlternativeDefinition


{- §7. Extensional Wellfounded Order -}

-- Lemma-56 : LEM → (A : Type) (_≺_ : A → A → Type) → isPropValued _≺_
--         →   (isTrans _≺_ × isExtensional _≺_ × isWellFounded _≺_)
--           ↔ ((P : A → Type) (a : A) → P a → ∃[ x ∈ A ] (P x × (∀ y → y ≺ x → ¬ P y)))

-- Lemma-57 : ((A B C : Ord) → A O.< B → B O.≤ C → A O.< C)
--          × (((A B C : Ord) → A O.≤ B → B O.< C → A O.< C) ↔ LEM)

-- Theorem-58 : isWellFounded O._<_ × isExtensional O._<_ × isTrans O._<_

-- Corollary-59 : isTrans O._<_ × isIrrefl O._<_
--              × isTrans O._≤_ × isRefl O._≤_ × isAntisym O._≤_
--              × ((A B C : Ord) → A O.< B → B O.≤ C → A O.< C)

Lemma-60 : O.is-zero ⓪ × O.calc-strong-suc (λ X → X O.+ ⑴)
      -- × ((X : Type) → O.has-sup-indexed-by X)
Lemma-60 = ⓪-is-zero , O.succ-calc-strong-suc

-- Theorem-61 : O.has-add × O.has-mul

-- Theorem-62 : O.has-sub ↔ LEM

-- Theorem-63 : ∀ {ℓ} →
--              (O.is-≤-monotone (λ X → X O.+ ⑴) ↔ LEM)
--            × (O.is-<-monotone (λ X → X O.+ ⑴) ↔ LEM)
--            × (isTrichotomous O._<_ ↔ LEM)
--            × (isConnex O._<_ ↔ LEM)
--            × (O.has-weak-classification ↔ LEM)
--            × (O.has-classification → LEM)
--            × (O.satisfies-classifiability-induction ℓ → LEM)

-- Theorem-64 : Splits Ord O._<_ O._≤_ ↔ LEM


{- §8. Interpretations Between the Notions -}

Theorem-65 : ({a b : Cnf} → a C.< b ↔ CtoB a B.< CtoB b)
           × ({a b : Cnf} → a C.≤ b ↔ CtoB a B.≤ CtoB b)
Theorem-65 = (CtoB-<-monotone , CtoB-reflects-<)
           , (CtoB-≤-monotone , CtoB-reflects-≤)

Corollary-66 : {a b : Cnf} → CtoB a ≡ CtoB b → a ≡ b
Corollary-66 = CtoB-injective

Theorem-67 : ((a b : Cnf) → CtoB (a C.+ b) ≡ CtoB a B.+ CtoB b)
           × ((a b : Cnf) → CtoB (a C.· b) ≡ CtoB a B.· CtoB b)
           × ((a   : Cnf) → CtoB (ω^⟨ a ⟩) ≡ ω^ (CtoB a))
Theorem-67 = CtoB-preserves-add
           , CtoB-preserves-mul
           , CtoB-preserves-exp-with-base-ω

Lemma-68 : (x : Cnf) → (p : C.is-lim x)
         → CtoB x ≡ limit (CtoB ∘ fund-sequence x p) {CtoB-preserves-increasing (fund-sequence↑ x p)}
Lemma-68 = CtoB-preserves-fund-sequence

Theorem-69 : (∀ {a} f f↑ → a C.is-lim-of (f , f↑) → CtoB a ≡ limit (CtoB ∘ f) {CtoB-preserves-increasing f↑})
           ↔ MP
Theorem-69 = CtoB-preserves-limits→MP , MP→CtoB-preserves-limits

Theorem-70 : (a : Cnf) → CtoB a B.< ε₀
Theorem-70 = CNF<ε₀

-- Lemma-71 : {X : Ord} →
--            ((x : Ord.Carrier X) → O.isSimulation {O.initial-segment X x} {X} fst)
--          × (∀ x y → (f : Ord.Carrier (O.initial-segment X x) → Ord.Carrier (O.initial-segment X y)) →
--              O.isSimulation {O.initial-segment X x} {O.initial-segment X y} f ↔ fst ∘ f ≡ fst)

Lemma-72 : ((a b : Brw) → a B.< b → BtoO a O.< BtoO b)
         × ((a b : Brw) → a B.≤ b → BtoO a O.≤ BtoO b)
      -- × ((a b : Brw) → BtoO a ≡ BtoO b → a ≡ b)
Lemma-72 = BtoO-<-monotone
         , BtoO-≤-monotone

-- Theorem-73 : ∀ {b a} → b O.< BtoO a →
--              Σ[ a' ∈ Brw ] (a' B.< a × (BtoO a' ≡ b))

-- Remark-74 : In the publisher's version, we erroneously claimed that BtoO being a simulation would imply WLPO.


{- §9. Computational Efficiency of our Notions of Ordinals -}

import Comparision.Hardy