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

has-zero : Type _
has-zero = Zer

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

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

has-strong-suc : Type _
has-strong-suc = Σ[ s  (A  A) ] calc-strong-suc s

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

IncrBoundedSeq : Type _
IncrBoundedSeq = Σ[ f  (  A) ] (is-<-increasing f × (Σ[ b  A ] (∀ k  f k < b)))

_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 

has-limits : Type _
has-limits = Σ[ lim  (IncrSeq  A) ]  f  lim f is-lim-of f

has-limits-of-bounded-sequences : Type _
has-limits-of-bounded-sequences = Σ[ lim  (IncrBoundedSeq  A) ]  f  lim f is-sup-of (fst f)

{- 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.
has-classification : Type _
has-classification = (a : A)  is-classifiable a

satisfies-classifiability-induction :    Type _
satisfies-classifiability-induction  =
   {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

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⟨has-classification⟩ : isProp has-classification
  isProp⟨has-classification⟩ = isPropΠ isProp⟨is-classifiable⟩


  {- Classifiability induction -}

  module ClassifiabilityInduction
    (cc : has-classification)
    (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))