----------------------------------------------------------------------------------------------------
-- 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  Σ-Π-≃ (isOfHLevelΠ  λ _ → 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 ) (fst p ))

  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 ) (<∘≤-in-< (<∘≤-in-< (f↑ ) (f≤a )) (is-z (f )))}

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