index.agda
----------------------------------------------------------------------------------------------------
-- 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