----------------------------------------------------------------------------------------------------
-- 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 hiding (∥_∥)
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 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))
 Lemma-4 = no-infinite-descending-sequence

 Corollary-5 : isWellFounded _<_
               {x y}  isProp ((x < y)  (x  y))
 Corollary-5 = wellfounded→reflexive-closure-is-prop A-is-set isProp⟨<⟩

 open import Abstract.ZerSucLim _<_ _≤_ as A

 Lemma-6 : (s : A  A) 
           (A.calc-suc s)  (∀ b x  ((b < x)  (s b  x)))
 Lemma-6 = A.Properties.calc-suc↔≤-<-characterization
           A-is-set isProp⟨<⟩ isProp⟨≤⟩ <-irrefl ≤-refl ≤-trans ≤-antisym <∘≤-in-<

 Lemma-7 : (a : A)  isProp (A.is-zero a  (A.is-strong-suc a  A.is-lim a))
 Lemma-7 = A.Properties.isProp⟨is-classifiable⟩
           A-is-set isProp⟨<⟩ isProp⟨≤⟩ <-irrefl ≤-refl ≤-trans ≤-antisym <∘≤-in-<

 Definition-8 :  {ℓ''}  Type _
 Definition-8 {ℓ''} = A.satisfies-classifiability-induction ℓ''

 Corollary-9 : A.satisfies-classifiability-induction _  A.has-classification
 Corollary-9 = A.Properties.classifiability-induction→has-classification
               A-is-set isProp⟨<⟩ isProp⟨≤⟩ <-irrefl ≤-refl ≤-trans ≤-antisym <∘≤-in-<

 Theorem-10 :  A.has-classification  isWellFounded _<_
              ℓ''  A.satisfies-classifiability-induction ℓ''
 Theorem-10 cl wf ℓ'' = A.Properties.ClassifiabilityInduction.ind
                        A-is-set isProp⟨<⟩ isProp⟨≤⟩ <-irrefl ≤-refl ≤-trans ≤-antisym <∘≤-in-<
                        cl wf {ℓ''}

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

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


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

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

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

 Theorem-16 : A.has-zero  A.has-suc  A.has-limits
             Discrete A  WLPO
 Theorem-16 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-17 : 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._≤_
Theorem-17 = 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

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

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

Lemma-20 : 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-20 = C.+-is-assoc , +r-is-<-monotone
         , C.·-is-assoc , ω^·-is-<-monotone
         , ·-is-left-distributive

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

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

Lemma-23 : (∀ 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-23 = C.Thm[sub]
         , C.Thm[div]

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

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

Theorem-26 :   
             C.has-classification
           × C.satisfies-classifiability-induction 
Theorem-26  = Cnf-has-classification , Cnf-satisfies-classifiability-induction 

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

Theorem-28 : (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-28 = Cnf-does-not-have-limits
           , LEM-computes-sup
           , having-limits-implies-WLPO


{- §6. Brouwer Ordinal Trees -}

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

Lemma-30 :  {x y}  x B.≤ y  B.succ x B.≤ B.succ y
Lemma-30 = ≤-succ-mono , ≤-succ-mono⁻¹

Lemma-31 :  x f {f↑}  x B.< limit f {f↑}   Σ[ n   ] x B.< f n 
Lemma-31 = B.below-limit-lemma

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

Lemma-33 : (∀ 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-33 = B.lim≤sx→lim≤x
         , x<lim→sx<lim

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

Theorem-35 : isAntisym B._≤_
Theorem-35 = λ _ _  B.≤-antisym

Corollary-36 : 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)
Corollary-36 = Brw-is-set ,  _ _  B.isProp⟨<⟩) ,  _ _  B.isProp⟨≤⟩)
             , B.<-trans , B.<-irreflexive
             ,  _ _ _  B.≤-trans) ,  _  B.≤-refl) ,  _ _  B.≤-antisym)
             , B.<∘≤-in-<

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

Lemma-38 : B.has-zero × B.has-strong-suc × B.has-limits
Lemma-38 = (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-39 : B.is-<-monotone B.succ
             × B.is-≤-monotone B.succ
Corollary-39 = <-succ-mono , ≤-succ-mono

Theorem-40 :   
             B.has-classification
           × B.satisfies-classifiability-induction 
Theorem-40  = Brw-has-classification , Brw-satisfies-classifiability-induction 

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

Lemma-42-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-42-i = B.+x-mono , B.·x-mono
--
Lemma-42-ii :  x {y z}  x B.+ y  x B.+ z  y  z
Lemma-42-ii = B.+-leftCancel
--
Lemma-42-iii : isAssoc B._+_
             × isAssoc B._·_
             × (∀ {x y} z  x B.· y B.+ x B.· z  x B.· (y B.+ z))
Lemma-42-iii =  _ _  B.+-assoc)
             ,  _ _  B.·-assoc)
             , B.·-+-distributivity
--
Lemma-42-iv :  x y z  x B.^ (y B.+ z)  x B.^ y B.· x B.^ z
Lemma-42-iv = λ x y z  B.exp-homomorphism {x} {y} {z}

Lemma-43 : (∀ 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-43 = B.additive-principal-ω^
         , B.additive-principal-ω^-closure
         , ω^x-absorbs-finite

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

Theorem-45 : (∀ 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-45 = decIsFinite
           , dec-n≡ , dec-≡n
           , dec-n< , dec-<n
           , dec-n≤ , dec-≤n

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

Theorem-47 : (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))  (∀   y  Dec (B.ω B.< y)))
           × ((∀   y  Dec (B.ω B.< y))  LPO)
           × (LPO                        Discrete Brw)
           × (Discrete Brw               (∀ x    Dec (  x  ω·2)))
           × ((∀ x    Dec (  x  ω·2))  LPO)
Theorem-47 = LPO→Dec≤
           , Dec≤→Dec<
           , Dec<→Decω<
           , Decω<→LPO
           , LPO→Dec≡
           , Dec≡→Dec≡ω·2
           , Dec≡ω·2→LPO

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

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

Theorem-50 :  (∀ x  Stable (x  B.ω))
           × ((∀ x  Stable (x  ω·2))  MP)
Theorem-50 = stable≡ω
           , stable≡ω·2→MP

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

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

Theorem-53 : (Σ[ _⊔_  (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-53 = (with-finite._⊔_ , with-finite.is-join)
           , (with-ω._⊔ω , with-ω.is-join)

Theorem-54 : (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-54 =  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-55 : ((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-56 : isExtensional O._<_ × isWellFounded O._<_ × isTrans O._<_

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

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

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

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

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

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


{- §8. Interpretations Between the Notions -}

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

Corollary-64 : {a b : Cnf}  CtoB a  CtoB b  a  b
Corollary-64 = CtoB-injective

Theorem-65 : ((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-65 = CtoB-preserves-add
           , CtoB-preserves-mul
           , CtoB-preserves-exp-with-base-ω

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

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

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

-- Lemma-69 : {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-70 : ((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-70 = BtoO-<-monotone
         , BtoO-≤-monotone

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

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


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

import Comparision.Hardy