----------------------------------------------------------------------------------------------------
-- Index of the Formalized Proofs in the paper
--
--     Connecting Constructive Notions of Ordinals in Homotopy Type Theory
--
--         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.Everything
open import Cubical.Data.Empty
open import Cubical.Data.Sum
open import Cubical.Data.Sigma
open import Cubical.Relation.Nullary
open import Cubical.Relation.Binary
open BinaryRelation
open import Cubical.Induction.WellFounded
  renaming (WellFounded to isWellFounded)

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.BrwToOrd

import Abstract.Arithmetic

Theorem-1 : isSet Cnf × isPropValued C._<_ × isPropValued C._≤_
          × isSet Brw × isPropValued B._<_ × isPropValued B._≤_
       -- × isSet Ord × isPropValued O._<_ × isPropValued O._≤_
          × isTrans C._<_ × isTrans C._≤_ × isIrrefl C._<_ × isRefl C._≤_ × isAntisym C._≤_
          × isTrans B._<_ × isTrans B._≤_ × isIrrefl B._<_ × isRefl B._≤_ × isAntisym B._≤_
       -- × isTrans O._<_ × isTrans O._≤_ × isIrrefl O._<_ × isRefl O._≤_ × isAntisym O._≤_
          × isTrichotomous C._<_ × isConvex C._≤_
       -- × (isTrichotomous O._<_ ↔ LEM) × (isConvex O._≤_ ↔ LEM)
Theorem-1 = Cnf-is-set , (λ _ _ → C.isProp⟨<⟩) , (λ _ _ → C.isProp⟨≤⟩)
          , Brw-is-set , (λ _ _ → B.isProp⟨<⟩) , (λ _ _ → B.isProp⟨≤⟩)
          , (λ _ _ _ → C.<-trans) , (λ _ _ _ → C.≤-trans) , (λ _ → C.<-irrefl) , (λ _ → C.≤-refl) , (λ _ _ → C.≤-antisym)
          , B.<-trans , (λ _ _ _ → B.≤-trans) , B.<-irreflexive , (λ _ → B.≤-refl) , (λ _ _ → B.≤-antisym)
          , C.<-tri , C.≤-connex


Theorem-2 : isExtensional C._<_ × isExtensional C._≤_
          × isExtensional B._<_ × isExtensional B._≤_
       -- × isExtensional O._<_ × isExtensional O._≤_
Theorem-2 = C.<-extensional , C.≤-extensional
          , B.<-extensional , B.≤-extensional


module _ {ℓ ℓ'} {A : Type ℓ} (_<_ : A → A → Type ℓ') where

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


Theorem-4 : isWellFounded C._<_
          × isWellFounded B._<_
       -- × isWellFounded O._<_
Theorem-4 = C.<-is-wellfounded
          , B.<-is-wellfounded


Theorem-5 : ({a b   : Cnf} → a C.< b → a C.≤ b)
          × ({a b c : Cnf} → a C.< b → b C.≤ c → a C.< c)
          × ({a b   : Brw} → a B.< b → a B.≤ b)
          × ({a b c : Brw} → a B.< b → b B.≤ c → a B.< c)
       -- × ({a b   : Ord} → a O.< b → a O.≤ b)
       -- × ({a b c : Ord} → a O.< b → b O.≤ c → a O.< c)
Theorem-5 = C.<-in-≤
          , C.<∘≤-in-<
          , B.<-in-≤
          , B.<∘≤-in-<


Theorem-6 : C.has-zero
          × B.has-zero
       -- × O.has-zero
Theorem-6 = Cnf-has-zero
          , Brw-has-zero


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

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

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


Theorem-8 : C.calc-strong-suc C.succ × C.is-<-monotone C.succ × C.is-≤-monotone C.succ
          × B.calc-strong-suc B.succ × B.is-<-monotone B.succ × B.is-≤-monotone B.succ
       -- × O.calc-strong-suc O.succ
       -- × (O.is-<-monotone O.succ ↔ LEM)
       -- × (O.is-≤-monotone O.succ ↔ LEM)
Theorem-8 = C.succ-calc-strong-suc , C.succ-is-<-monotone , C.succ-is-≤-monotone
          , B.succ-calc-strong-suc , B.<-succ-mono , B.≤-succ-mono


Theorem-9 : (C.has-limits → ⊥)
          × B.has-limits -- (of increasing sequences)
       -- × ((f : ℕ → Ord) → is-≤-increasing f → Σ[ a ∈ Ord ] a is-sup-of f)
       -- × (LEM → C.has-limits-of-bounded-sequences)
       -- × (C.has-limits-of-bounded-sequences → WLPO)
Theorem-9 = Cnf-does-not-have-limits
          , Brw-has-limits


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

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

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


Theorem-11 : C.has-classification
           × B.has-classification
        -- × (O.has-classification → LEM)
Theorem-11 = Cnf-has-classification
           , Brw-has-classification

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

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

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


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


Theorem-14 : ∀ ℓ → C.satisfies-classifiability-induction ℓ
                 × B.satisfies-classifiability-induction ℓ
              -- × (O.satisfies-classifiability-induction ℓ → LEM)
Theorem-14 ℓ = Cnf-satisfies-classifiability-induction ℓ
             , Brw-satisfies-classifiability-induction ℓ


module _ {ℓ ℓ'}(A : Type ℓ)(_<_ _≤_   : A → A → Type ℓ') where

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


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


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


Theorem-18 : C.has-unique-add × C.has-unique-mul × C.has-unique-exp-with-base C.ω
           × B.has-unique-add × B.has-unique-mul × B.has-unique-exp
        -- × O.has-add × O.has-mul
Theorem-18 = Cnf-has-unique-add , Cnf-has-unique-mul , Cnf-has-unique-exp-with-base-ω
           , Brw-has-unique-add , Brw-has-unique-mul , Brw-has-unique-exp


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


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


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


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


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


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


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