```----------------------------------------------------------------------------------------------------
-- An axiomatic approach to ordinals
----------------------------------------------------------------------------------------------------

{- A set `A` with relations `<` and `≤` satisfying certain conditions
allow us to define standard concepts of ordinals. This means that
we treat `A` as some sort of "abstract ordinal". -}

{-# OPTIONS --cubical --safe #-}

open import Cubical.Foundations.Prelude

module Abstract.ZerSucLim
{i j k}
{A : Type i}
(_<_ : A → A → Type j)
(_≤_ : A → A → Type k)
where

open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Function
open import Cubical.Data.Sigma
open import Cubical.Data.Nat
open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Sum
open import Cubical.Data.Empty
open import Cubical.Data.Sigma
open import Cubical.Relation.Nullary
open import Cubical.Relation.Binary
open BinaryRelation renaming (isTrans to isTransitive ; isRefl to isReflexive)
open import Cubical.HITs.PropositionalTruncation.Properties
renaming (rec to ∥-∥rec)
open import Cubical.Induction.WellFounded
renaming (WellFounded to isWellFounded;
Acc to isAcc)
open import Iff

{- monotonicity definition -}

is-<-monotone : (f : A → A) → Type _
is-<-monotone f = (b a : A) → b < a → f b < f a

is-≤-monotone : (f : A → A) → Type _
is-≤-monotone f = (b a : A) → b ≤ a → f b ≤ f a

is-pointwise-≤-monotone : ((ℕ → A) → A) → Type _
is-pointwise-≤-monotone ⊔ = (f g : ℕ → A) → (∀ n → f n ≤ g n) → ⊔ f ≤ ⊔ g

{- increasing definition -}

is-<-increasing : (ℕ → A) → Type _
is-<-increasing f = ∀ k → f k < f (suc k)

is-≤-increasing : (ℕ → A) → Type _
is-≤-increasing f = ∀ k → f k ≤ f (suc k)

{- Zero -}

is-zero : A → Type _
is-zero a = (b : A) → a ≤ b

Zer : Type _
Zer = Σ[ a ∈ A ] (is-zero a)

{- Successor -}

_is-suc-of_ : A → A → Type _
a is-suc-of b = (b < a) × (∀ x → b < x → a ≤ x)

calc-suc : (s : A → A) → Type _
calc-suc s = (b : A) → (s b) is-suc-of b

have-suc : Type _
have-suc = Σ[ s ∈ (A → A) ] calc-suc s

is-suc : A → Type _
is-suc a = ∃[ b ∈ A ] a is-suc-of b

{- Predecessor and strong successor -}
-- (predecessor is not used, but the strong successor is central)

_is-pred-of_ : A → A → Type _
b is-pred-of a = (b < a) × (∀ x → x < a → x ≤ b)

_is-strong-suc-of_ : A → A → Type _
a is-strong-suc-of b = a is-suc-of b × ∀ x → x < a → x ≤ b

is-strong-suc : A → Type _
is-strong-suc a = Σ[ b ∈ A ] a is-strong-suc-of b

{- Supremum -}

_is-sup-of_ : A → (ℕ → A) → Type _
a is-sup-of f = (∀ i → f i ≤ a) × (∀ x → ((∀ i → f i ≤ x) → a ≤ x))

calc-sup : ((ℕ → A) → A) → Type _
calc-sup ⊔ = ∀ f → (⊔ f) is-sup-of f

has-sup : Type _
has-sup = Σ[ ⊔ ∈ ((ℕ → A) → A) ] calc-sup ⊔

-- Remark: other definition of supremum (not used)
_is-sup∃-of_ : A → (ℕ → A) → Type _
a is-sup∃-of f = (∀ i → f i ≤ a) × (∀ x → (x < a → ∃[ i ∈ ℕ ] x ≤ f i))

{- Limits -}

IncrSeq : Type _
IncrSeq = Σ[ f ∈ (ℕ → A) ] is-<-increasing f

_is-lim-of_ : A → IncrSeq → Type _
a is-lim-of (f , _) = a is-sup-of f

is-Σlim : A → Type _
is-Σlim a = Σ[ f ∈ IncrSeq ] a is-lim-of f

is-lim : A → Type _
is-lim a = ∥ is-Σlim a ∥

{- Classifiability -}

is-classifiable : A → Type _
is-classifiable a = is-zero a ⊎ (is-strong-suc a ⊎ is-lim a)

is-Σclassifiable : A → Type _
is-Σclassifiable a = is-zero a ⊎ (is-strong-suc a ⊎ is-Σlim a)

to-is-classifiable : {a : A} → is-Σclassifiable a → is-classifiable a
to-is-classifiable (inl x) = inl x
to-is-classifiable (inr (inl x)) = inr (inl x)
to-is-classifiable (inr (inr x)) = inr (inr ∣ x ∣)

not-zs-is-lim : {a : A} → is-Σclassifiable a
→ ¬ (is-zero a) → ¬ (is-strong-suc a) → is-Σlim a
not-zs-is-lim (inl x)       f g = ⊥.rec (f x)
not-zs-is-lim (inr (inl x)) f g = ⊥.rec (g x)
not-zs-is-lim (inr (inr x)) f g = x

-- We say that (A , < , ≤) is classifiable if every `a : A` is.
is-completely-class : Type _
is-completely-class = (a : A) → is-classifiable a

module Properties
(A-is-set : isSet A)
(isProp⟨<⟩ : isPropValued _<_)
(isProp⟨≤⟩ : isPropValued _≤_)
(<-irrefl : (a : A) → ¬ (a < a))
(≤-refl : isReflexive _≤_)
(≤-trans : isTransitive _≤_)
(≤-antisym : {a b : A} → a ≤ b → b ≤ a → a ≡ b)
(<∘≤-in-< : {a b c : A} → a < b → b ≤ c → a < c)
where

private
≤-reflexive : {a b : A} → a ≡ b → a ≤ b
≤-reflexive {a} {b} p = subst (a ≤_) p (≤-refl a)

isProp⟨is-zero⟩ : (a : A) → isProp (is-zero a)
isProp⟨is-zero⟩ a = isPropΠ λ _ → isProp⟨≤⟩ _ _

isProp⟨Zer⟩ : isProp Zer
isProp⟨Zer⟩ (a₁ , p₁) (a₂ , p₂) = Σ≡Prop isProp⟨is-zero⟩ (≤-antisym (p₁ a₂) (p₂ a₁))

isProp⟨is-suc-of⟩ : {a b : A} → isProp (a is-suc-of b)
isProp⟨is-suc-of⟩ =
isProp× (isProp⟨<⟩ _ _)
(isPropΠ λ _ → isPropΠ λ _ → isProp⟨≤⟩ _ _)

isProp⟨calc-suc⟩ : (s : A → A) → isProp (calc-suc s)
isProp⟨calc-suc⟩ s = isPropΠ λ _ → isProp⟨is-suc-of⟩

suc-unique : (b : A) → isProp (Σ[ a ∈ A ] (a is-suc-of b))
suc-unique b (a₁ , b<a₁ , a₁-min) (a₂ , b<a₂ , a₂-min) =
Σ≡Prop (λ _ → isProp⟨is-suc-of⟩) (≤-antisym (a₁-min a₂ b<a₂) (a₂-min a₁ b<a₁))

isProp⟨have-suc⟩ : isProp have-suc
isProp⟨have-suc⟩ = isOfHLevelRespectEquiv 1 Σ-Π-≃ (isOfHLevelΠ 1 λ _ → suc-unique _)

isProp⟨is-suc⟩ : {a : A} → isProp (is-suc a)
isProp⟨is-suc⟩ = propTruncIsProp

isProp⟨is-strong-suc-of⟩ : {a b : A} → isProp (a is-strong-suc-of b)
isProp⟨is-strong-suc-of⟩ =
isProp× isProp⟨is-suc-of⟩
(isPropΠ2 λ _ _ → isProp⟨≤⟩ _ _ )

isProp⟨is-strong-suc⟩ : {a : A} → isProp (is-strong-suc a)
isProp⟨is-strong-suc⟩ {a} (b₁ , is-suc₁ , is-pred₁) (b₂ , is-suc₂ , is-pred₂) =
Σ≡Prop (λ _ → isProp⟨is-strong-suc-of⟩)
(≤-antisym (is-pred₂ b₁ (fst is-suc₁)) (is-pred₁ b₂ (fst is-suc₂)))

-- A useful lemma:
-- a function s calculates successors IFF b < a ↔ s b ≤ a
calc-suc↔≤-<-characterization : (s : A → A) →
(calc-suc s)
↔
((b a : A) → ((b < a) ↔ (s b ≤ a)))
calc-suc↔≤-<-characterization s =
(λ s-is-suc b a → snd (s-is-suc b) a ,
λ sb≤a → <∘≤-in-< (fst (s-is-suc b)) sb≤a)
,
λ char b → snd (char b (s b)) (≤-refl (s b)) ,
λ a → fst (char b a)

isProp⟨is-sup-of⟩ : ∀ {a f} → isProp (a is-sup-of f)
isProp⟨is-sup-of⟩ = isProp× (isPropΠ λ _ → isProp⟨≤⟩ _ _) (isPropΠ2 λ _ _ → isProp⟨≤⟩ _ _)

isProp⟨calc-sup⟩ : (⊔ : (ℕ → A) → A) → isProp (calc-sup ⊔)
isProp⟨calc-sup⟩ ⊔ = isPropΠ λ _ → isProp⟨is-sup-of⟩

isProp⟨has-sup⟩ : isProp has-sup
isProp⟨has-sup⟩ (⊔₁ , proof₁) (⊔₂ , proof₂) =
Σ≡Prop (λ _ → isProp⟨calc-sup⟩ _)
(funExt {f = ⊔₁} {g = ⊔₂} λ f →
≤-antisym (snd (proof₁ f) (⊔₂ f) (fst (proof₂ f)))
(snd (proof₂ f) (⊔₁ f) (fst (proof₁ f))))

sup-zero : ∀ {a f} → is-zero a → a is-sup-of f → ∀ n → f n ≡ a
sup-zero {a} {f} p q n = ≤-antisym (fst q n) (p (f n))

sup-constant : ∀ {a c f} → a is-sup-of f → (∀ n → f n ≡ c) → a ≡ c
sup-constant {a} {c} p q = ≤-antisym (snd p c (≤-reflexive ∘ q)) (subst (_≤ a) (q 0) (fst p 0))

sup-unique : ∀ {a b f} → a is-sup-of f → b is-sup-of f → a ≡ b
sup-unique {a} {b} {f} (f≤a , a-min-over-f) (f≤b , b-min-over-f) = ≤-antisym a≤b b≤a
where
a≤b : a ≤ b
a≤b = a-min-over-f b f≤b
b≤a : b ≤ a
b≤a = b-min-over-f a f≤a

isProp⟨is-lim⟩ : {a : A} → isProp (is-lim a)
isProp⟨is-lim⟩ = propTruncIsProp

-- `a : A` can only be one out of {zero, strong successor, limit}.
-- We first show that `a` can't be two out of {zero, strong successor, limit} at the same time.
module unique (a : A) where

-- Easy: `a` can't be zero and strong successor simultaneously.
not-z-and-s : (is-zero a) → (is-strong-suc a) → ⊥
not-z-and-s is-z (b , (b<a , _) , _) = <-irrefl b (<∘≤-in-< b<a (is-z b))

-- `a` can't be zero and limit.
-- We need to eliminate out of the propositional truncation. In cubical Agda, we can choose
-- whether we use the "old-style" truncation recursion principle, proved in the library, or
-- the new pattern matching for HITs. Here, we use the old-style principle;
-- for the suc-lim case below, we use the new pattern matching.
not-z-and-l : (is-zero a) → (is-lim a) → ⊥
not-z-and-l is-z = ∥-∥rec isProp⊥ λ { ((f , f↑) , f≤a , _) →
<-irrefl (f 0) (<∘≤-in-< (<∘≤-in-< (f↑ 0) (f≤a 1)) (is-z (f 0)))}

-- The hardest case: `a` can't be strong successor and limit simultaneously.
not-s-and-l : (is-strong-suc a) → (is-lim a) → ⊥
not-s-and-l (b , (b<a , a-min-over-b) , b-max) ∣ (f , f↑) , f≤a , a-min-over-f ∣ = <-irrefl b b<b
where
f≤b : (n : ℕ) → f n ≤ b
f≤b n = b-max (f n) (<∘≤-in-< (f↑ n) (f≤a (suc n)))
a≤b : a ≤ b
a≤b = a-min-over-f b f≤b
b<b : b < b
b<b = <∘≤-in-< b<a a≤b
not-s-and-l a-str-suc (∥_∥.squash fl₁ fl₂ i) = isProp⊥ (not-s-and-l a-str-suc fl₁)
(not-s-and-l a-str-suc fl₂) i
open unique

-- Uniqueness of classification. We simply put everything from above together.
-- ⊎ is not declared left or right associative, thus we need brackets in the statement.
isProp⟨is-classifiable⟩ : (a : A) → isProp (is-classifiable a)
isProp⟨is-classifiable⟩ a (inl z₁) (inl z₂) =
cong inl (isProp⟨is-zero⟩ a _ _)
isProp⟨is-classifiable⟩ a (inl z₁) (inr (inl s₂)) =
⊥.elim {A = λ _ → (inl z₁) ≡ inr (inl {B = is-lim a} s₂)} (not-z-and-s a z₁ s₂)
isProp⟨is-classifiable⟩ a (inl z₁) (inr (inr l₂)) =
⊥.elim {A = λ _ → (inl z₁) ≡ inr (inr {A = is-strong-suc a} l₂)} (not-z-and-l a z₁ l₂)
isProp⟨is-classifiable⟩ a (inr (inl s₁)) (inl z₂) =
sym (isProp⟨is-classifiable⟩ a (inl z₂) (inr (inl s₁)))
isProp⟨is-classifiable⟩ a (inr (inl s₁)) (inr (inl s₂)) =
cong inr (cong inl (isProp⟨is-strong-suc⟩ s₁ s₂))
isProp⟨is-classifiable⟩ a (inr (inl s₁)) (inr (inr l₂)) =
⊥.elim {A = λ _ → (inr {A = is-zero a} (inl s₁)) ≡ (inr (inr l₂))} (not-s-and-l a s₁ l₂)
isProp⟨is-classifiable⟩ a (inr (inr l₁)) (inl z₂) =
sym (isProp⟨is-classifiable⟩ a (inl z₂) (inr (inr l₁)))
isProp⟨is-classifiable⟩ a (inr (inr l₁)) (inr (inl s₂)) =
sym (isProp⟨is-classifiable⟩ a (inr (inl s₂)) (inr (inr l₁)))
isProp⟨is-classifiable⟩ a (inr (inr l₁)) (inr (inr l₂)) =
cong inr (cong inr (isProp⟨is-lim⟩ l₁ l₂))

isProp⟨is-completely-class⟩ : isProp is-completely-class
isProp⟨is-completely-class⟩ = isPropΠ isProp⟨is-classifiable⟩

{- Classifiability induction -}

module ClassifiabilityInduction
(cc : is-completely-class)
(wf : isWellFounded _<_)
where

ind : ∀ {ℓ} {P : A → Type ℓ}
→ (∀ a → isProp (P a))
→ (∀ a → is-zero a → P a)
→ (∀ a b → a is-strong-suc-of b → P b → P a)
→ (∀ a f f↑ → a is-lim-of (f , f↑) → (∀ i → P (f i)) → P a)
→ ∀ a → P a
ind {_} {P} pvP pz ps pl = WFI.induction wf step
where
step : ∀ a → (∀ b → b < a → P b) → P a
step a h with cc a
... | inl a-is-zero = pz a a-is-zero
... | inr (inl (b , a-is-suc-of-b)) = ps a b a-is-suc-of-b (h b (fst (fst a-is-suc-of-b)))
... | inr (inr a-is-lim) = ∥-∥rec (pvP a) claim a-is-lim
where
claim : is-Σlim a → P a
claim ((f , f↑) , a-is-sup-of-f) = pl a f f↑ a-is-sup-of-f (λ i → h (f i) (f<a i))
where
f<a : ∀ i → f i < a
f<a i = <∘≤-in-< (f↑ i) (fst a-is-sup-of-f (suc i))
```