```----------------------------------------------------------------------------------------------------
-- 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-16 : Type _
Definition-16 =

Definition-17 : Type _
Definition-17 =

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
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))
, 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
```