----------------------------------------------------------------------------------------------------
-- Classifiability of Extensional Wellfounded Orders
----------------------------------------------------------------------------------------------------
{-# OPTIONS --cubical #-}

module ExtensionalWellfoundedOrder.Classifiability where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Induction.WellFounded
  renaming (WellFounded to isWellFounded)

open import Cubical.Data.Empty
open import Cubical.Data.Unit
open import Cubical.Data.Sum
open import Cubical.Data.Sigma
open import Cubical.HITs.SetQuotients

open import ExtensionalWellfoundedOrder.Base
open import ExtensionalWellfoundedOrder.Arithmetic

open import Abstract.ZerSucLim _<_ _≤_ public

open import PropTrunc

open Ord
open _≤_
open _<_
open isSimulation

{- Small lemmas on left injections -}

IsLeft : {A B : Type} → A ⊎ B → Type
IsLeft {A} x = Σ[ a ∈ A ] x ≡ inl a

isleft : {A B : Type} → (a : A) → IsLeft {A} {B} (inl a)
isleft a = (a , refl)

injInl : {A B : Type} → {a a' : A} → inl {B = B} a ≡ inl a' → a ≡ a'
injInl {a = a} {a'} p = lower (⊎Path.encode _ _ p)

{- Zero -}

⓪ : Ord
Carrier ⓪ = ⊥
_≺_ ⓪ () y
truncated ⓪ () b
wellfounded ⓪ ()
extensional ⓪ () b
transitive ⓪ () b c

⓪-is-zero : is-zero ⓪
f (⓪-is-zero b) = λ ()
monotone (f-simulation (⓪-is-zero b)) {()}
simulation (f-simulation (⓪-is-zero b)) {a = ()}

Ord-has-zero : has-zero
Ord-has-zero = ⓪ , ⓪-is-zero

{- Successor -}

⑴ : Ord
Carrier ⑴ = Unit
_≺_ ⑴ _ _ = ⊥
truncated ⑴ x y () q
wellfounded ⑴ _ = acc λ y ()
extensional ⑴ _ _ _ = refl
transitive ⑴ a b c () q

succ : Ord → Ord
succ A = A + ⑴

succ-calc-strong-suc : (A : Ord) → succ A is-strong-suc-of A
succ-calc-strong-suc A = (A<succA , lub) , lub'
  where
    A<succA : A < succ A
    f (sim A<succA) = inl
    monotone (f-simulation (sim A<succA)) p = p
    simulation (f-simulation (sim A<succA)) {inl a} p = a , p , refl
    bound A<succA = inr tt
    bounded A<succA a = tt
    equiv A<succA = isoToIsEquiv (iso (λ a → (inl a) , tt) g s r)
      where
        g : Σ (Carrier A ⊎ Unit) _ → Carrier A
        g (inl x , _) = x
        g (inr x , ())
        s : section (λ a → inl a , tt) g
        s (inl x , p) = refl
        s (inr x , ())
        r : retract (λ a → inl a , tt) g
        r a = refl

    lub : (X : Ord) → A < X → succ A ≤ X
    f (lub X A<X) (inl a) = f (sim A<X) a
    f (lub X A<X) (inr _) = bound A<X
    monotone (f-simulation (lub X A<X)) {inl a} {inl a'} p = monotone (sim A<X) p
    monotone (f-simulation (lub X A<X)) {inl a} {inr a'} p = bounded A<X a
    simulation (f-simulation (lub X A<X)) {a} {inl a'} p
      = let (x , q) = simulation (sim A<X) p in ((inl x) , q)
    simulation (f-simulation (lub X A<X)) {x} {inr _} p = (inl a) , _ , eq
      where
        a = Iso.inv (equivToIso (_ , equiv A<X)) (x , p)
        eq = cong fst (Iso.rightInv (equivToIso (_ , equiv A<X)) (x , p))

    f-below-bound : (X : Ord) → (X<SA : X < succ A) → ∀ x → IsLeft (f (sim X<SA) x)
    f-below-bound X X<SA x = helper X X<SA x (Iso.fun (equivToIso (_ , equiv X<SA)) x) (Iso.leftInv (equivToIso (_ , equiv X<SA)) x)
      where
        helper : ∀ {A} X (X<SA : X < (A + ⑴)) (x : Carrier X)
           (w : Σ (Carrier A ⊎ Unit) (λ y → ((A + ⑴) ≺ y) (bound X<SA))) →
         equiv X<SA .equiv-proof w .fst .fst ≡ x → IsLeft (f (sim X<SA) x)
        helper X X<SA x (inl a , q) r = subst IsLeft (sym (cong fst (Iso.rightInv (equivToIso (_ , equiv X<SA)) (inl a , q))) ∙ cong (f (sim X<SA)) r) (isleft a)
        helper X X<SA x (inr _ , q) r = helperhelper X X<SA x (bound X<SA) q
          where
           helperhelper : ∀ {A} {x} X (X<SA : X < (A + ⑴)) (x₁ : Carrier X) (w : Carrier A ⊎ Unit) → ((A + ⑴) ≺ inr x) w → IsLeft (f (sim X<SA) x₁)
           helperhelper X X<SA x (inl x₁) ()
           helperhelper X X<SA x (inr x₁) ()

    lub' : (X : Ord) → X < succ A → X ≤ A
    f (lub' X X<SA) x with f-below-bound X X<SA x
    ... | (a , p) = a
    monotone (f-simulation (lub' X X<SA)) {x} {x'} p with f-below-bound X X<SA x | f-below-bound X X<SA x'
    monotone (f-simulation (lub' X X<SA)) {x} {x'} p | (a , q) | (a' , q') = subst2 (_≺_ (A + ⑴)) q q' (monotone (sim X<SA) p)
    simulation (f-simulation (lub' X X<SA)) {a} {x} p with f-below-bound X X<SA x
    simulation (f-simulation (lub' X X<SA)) {a} {x} p | (a' , q') with simulation (sim X<SA) {inl a} {x} (subst (_≺_ (A + ⑴) (inl a)) (sym q') p)
    simulation (f-simulation (lub' X X<SA)) {a} {x} p | (a' , q') | (x' , (x'<x , r)) = x' , x'<x , lem
      where
        lem : f (lub' X X<SA) x' ≡ a
        lem with f-below-bound X X<SA x'
        ... | (a'' , q'') = injInl (sym q'' ∙ r)

Ord-has-strong-suc : has-strong-suc
Ord-has-strong-suc = succ , succ-calc-strong-suc