open import Cubical.Foundations.Prelude

module SignatureAlgebra.Initial.Elimination (ℓi : Level) where

open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Structure

open import Cubical.Data.Sigma

open import Cubical.HITs.PropositionalTruncation hiding (rec)

open import DCPO ℓi

open import SignatureAlgebra.Initial.Base ℓi
open import SignatureAlgebra.Signature ℓi
open import SignatureAlgebra.SignatureAlgebra ℓi
open import SignatureAlgebra.Monomial ℓi

private
  variable
    ℓc ℓmb ℓmc ℓmct ℓe ℓv ℓa ℓt : Level

module _ {Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv} (A : SignatureAlgebra Σ ℓa ℓt) where
  {- NOTE:
    We need to annotate `rec` and `recIsMonotone` with a TERMINATING pragma,
    as the type checker does not believe that `rec` and `recIsMonotone` terminate.
    This has to do with the fact that Agda fails to recognize that certain recursive calls are structural,
    especially when these calls are made in other functions.

    We already unfolded some definitions, to make sure that less errors occur when we remove this pragma,
    but it still doesn't fully convince the type checker.

    The remaining cases which aren't accepted are:
    - recIsMonotone (appIsUpperbound c α δ i)
    - recIsMonotone (appIsLowerboundOfUpperbounds c α δ v vIsUpper)
    - recIsMonotone (inequality j ρ)
    We describe what goes wrong at their definitions, and why they should be accepted. -}
  {-# TERMINATING #-}
  rec : Initial Σ → ⟨ A ⟩
  recIsMonotone : isMonotone (initialSignatureDCPO Σ) (underlyingDCPO A) rec
  recCommutes : isCommutingWithInterpretation (initialSignatureAlgebra Σ) A rec

  {- NOTE:
    This is basically the same as
      isMonotone→imageIsDirected (initialSignatureDCPO Σ) (underlyingDCPO A)
        rec recIsMonotone δ
    but we need to unfold it (and the definition of ∥₁.map as well) for the
    termination checker to accept it -}
  recImageIsDirected : {I : Type ℓi} {α : I → Initial Σ}
                     → isDirected (Leq Σ) α
                     → isDirected (algebraOrder A) (rec ∘ α)
  recImageIsDirected {I = I} {α = α} δ =
    inhabitedIfDirected (Leq Σ) δ ,
    {- NOTE:
      We would prefer to write `semidirectedIfDirected (Leq Σ) δ` instead
      of `snd δ i j`, but writing it like this, makes Agda realize that
      αᵢ⊑αₖ, αⱼ⊑αₖ are actually structurally smaller than δ, so we are
      allowed to make a recursive call on them. -}
    λ i j → h i j (snd δ i j)
    where
      h : (i j : I)
        → ∃[ k ∈ I ] α i ⊑[ Σ ] α k ×
                     α j ⊑[ Σ ] α k
        → ∃[ k ∈ I ] rec (α i) ⊑⟨ underlyingDCPO A ⟩ rec (α k) ×
                     rec (α j) ⊑⟨ underlyingDCPO A ⟩ rec (α k)
      h i j ∣ k , αᵢ⊑αₖ , αⱼ⊑αₖ ∣₁ = ∣ k , recIsMonotone αᵢ⊑αₖ , recIsMonotone αⱼ⊑αₖ ∣₁
      h i j (squash₁ x y k) = squash₁ (h i j x) (h i j y) k

  rec (app c args) =
    {- NOTE:
      The following two terms are definitionally equal:
      - fmapₘ (constructors Σ c) (initialSignatureDCPO Σ) (underlyingDCPO A) rec args
      - rec ∘ fst args , snd args
      However, the termination checker fails to accept this function if
      we write the former. -}
    interpretation A c (rec ∘ fst args , snd args)
  rec (lub {α = α} δ) =
    ∐ (underlyingDCPO A) {α = rec ∘ α} (recImageIsDirected δ)
  rec (leqAntiSym x y x⊑y y⊑x i) =
    antisymmetry (underlyingDCPO A) (rec x) (rec y)
      (recIsMonotone x⊑y)
      (recIsMonotone y⊑x)
      i
  rec (isSetInitial x y p q i j) =
    sethood (underlyingDCPO A) (rec x) (rec y) (cong rec p) (cong rec q) i j

  {- NOTE:
    We need to prove that
      rec (app c (α i))
        ⊑⟨ underlyingDCPO A ⟩
      rec (app c (∐ (⟦ constructors Σ c ⟧ₘ (initialSignatureDCPO Σ)) δ))
    i.e.
      interpretation A c (fmapₘ (constructors Σ c) (initialSignatureDCPO Σ) (underlyingDCPO A) rec (α i))
        ⊑⟨ A ⟩
      interpretation A c (fmapₘ (constructors Σ c) (initialSignatureDCPO Σ) (underlyingDCPO A) rec (∐ (⟦ constructors Σ c ⟧ₘ (initialSignatureDCPO Σ)) δ))
    If we unfold these definitions, we have to reason with the term
      rec ∘ fst (∐ (⟦ constructors Σ c ⟧ₘ (initialSignatureDCPO Σ)) δ)
    The problem is that Agda does not like this term, as
      fst (∐ (⟦ constructors Σ c ⟧ₘ (initialSignatureDCPO Σ)) δ)
    is not structurally smaller than
      appIsUpperbound c α δ i

    However, as `interpretation A c` is continuous, it suffices to show that
      fmapₘ (constructors Σ c) (initialSignatureDCPO Σ) (underlyingDCPO A) rec (α i)
        ⊑⟨ ⟦ constructors Σ c ⟧ₘ (initialSignatureDCPO Σ) ⟩
      fmapₘ (constructors Σ c) (initialSignatureDCPO Σ) (underlyingDCPO A) rec (∐ (⟦ constructors Σ c ⟧ₘ (initialSignatureDCPO Σ)) δ)
    i.e.
      (rec ∘ fst (α i), snd (α i))
        ⊑⟨ ⟦ constructors Σ c ⟧ₘ (initialSignatureDCPO Σ) ⟩
      (rec ∘ fst (∐ (⟦ constructors Σ c ⟧ₘ (initialSignatureDCPO Σ)) δ), snd (∐ (⟦ constructors Σ c ⟧ₘ (initialSignatureDCPO Σ)) δ))

    Informally, if we unfold `⟦ constructors Σ c ⟧ₘ (initialSignatureDCPO Σ)`, this amounts to showing that
      (1) ∀ b : B. rec (fst (α i) b) ⊑⟨ A ⟩ rec (lub (λ i → fst (α i) b))
                                    =      ∐ (λ i → rec (fst (α i) b))
      (2) snd (α i) ⊑⟨ C ⟩ ∐ snd ∘ α
    To show that `(λ i → rec (fst (α i) b))` is directed, we do need to make recursive calls to `recIsMonotone`.
    However, that should be allowed here, as `fst (α i) b` is structurally smaller.
  -}
  recIsMonotone (appIsUpperbound c α δ i) =
    isContinuous→isMonotone
      (⟦ constructors Σ c ⟧ₘ (underlyingDCPO A)) (underlyingDCPO A)
      (interpretation A c) (interpretationIsContinuous A c)
      (fmapₘisMonotone (constructors Σ c)
        (initialSignatureDCPO Σ) (underlyingDCPO A)
        rec recIsMonotone
        (∐isUpperbound (⟦ constructors Σ c ⟧ₘ (initialSignatureDCPO Σ)) δ i))

  {- NOTE:
    This suffers from the same problem as `recIsMonotone (appIsUpperbound c α δ i)`,
    where Agda does not like it that we use `recIsMonotone` to show that
      fmapₘ (constructors Σ c) (initialSignatureDCPO Σ) (underlyingDCPO A) rec ∘ α
    is directed. However, again, if we unfold the definitions, we only make recursive calls on structurally smaller arguments. -}
  recIsMonotone (appIsLowerboundOfUpperbounds c α δ v vIsUpper) =
    subst (λ - → - ⊑⟨ underlyingDCPO A ⟩ rec v)
      p
      (supIsLowerboundOfUpperbounds (order (underlyingDCPO A))
        (interpretationIsContinuous A c _ _ ε)
        (rec v)
        recvIsUpperbound)
    where
      ε : isDirected (order (⟦ constructors Σ c ⟧ₘ (underlyingDCPO A)))
            (fmapₘ (constructors Σ c) (initialSignatureDCPO Σ) (underlyingDCPO A) rec ∘ α)
      ε = isMonotone→imageIsDirected
            (⟦ constructors Σ c ⟧ₘ (initialSignatureDCPO Σ))
            (⟦ constructors Σ c ⟧ₘ (underlyingDCPO A))
            (fmapₘ (constructors Σ c) (initialSignatureDCPO Σ) (underlyingDCPO A) rec)
            (fmapₘisMonotone (constructors Σ c)
              (initialSignatureDCPO Σ) (underlyingDCPO A)
              rec recIsMonotone)
            δ

      p : interpretation A c (∐ (⟦ constructors Σ c ⟧ₘ (underlyingDCPO A)) ε)
        ≡ rec (app c (∐ (⟦ constructors Σ c ⟧ₘ (initialSignatureDCPO Σ)) δ))
      p =
        cong (interpretation A c)
          (≡-×
            (funExt λ b →
              cong (∐ (underlyingDCPO A))
                (isPropIsDirected (order (underlyingDCPO A)) _ _ _))
            (cong (∐ (Monomial.C (constructors Σ c)))
              (isPropIsDirected (order (Monomial.C (constructors Σ c))) _ _ _)))

      recvIsUpperbound :
        isUpperbound (order (underlyingDCPO A))
          (rec v)
          (interpretation A c ∘
            fmapₘ (constructors Σ c) (initialSignatureDCPO Σ) (underlyingDCPO A) rec ∘
            α)
      recvIsUpperbound i = recIsMonotone (vIsUpper i)

  recIsMonotone (leqRefl x) = reflexivity (underlyingDCPO A) (rec x)
  recIsMonotone (leqTrans x y z x⊑y y⊑z) =
    transitivity (underlyingDCPO A)
      (rec x) (rec y) (rec z) (recIsMonotone x⊑y) (recIsMonotone y⊑z)
  recIsMonotone (lubIsUpperbound {α = α} δ i) =
    ∐isUpperbound (underlyingDCPO A) {α = rec ∘ α} (recImageIsDirected δ) i
  recIsMonotone (lubIsLowerboundOfUpperbounds {α = α} δ v vIsUpper) =
    ∐isLowerBoundOfUpperbounds (underlyingDCPO A) {α = rec ∘ α} _
      (rec v) (recIsMonotone ∘ vIsUpper)
  recIsMonotone (isPropLeq x y x⊑y x⊑y' i) =
    isProp→PathP (λ i → propValuedness (underlyingDCPO A) (rec x) (rec y))
      (recIsMonotone x⊑y) (recIsMonotone x⊑y') i

  {- NOTE:
    We need to prove that
      rec (⟦ lhs (inequalities Σ j) ⟧ₜ (initialSignatureDCPO Σ) app ρ)
        ⊑⟨ underlyingDCPO A ⟩
      rec (⟦ rhs (inequalities Σ j) ⟧ₜ (initialSignatureDCPO Σ) app ρ)
    The problem is that Agda does not like these terms, as
      ⟦ lhs (inequalities Σ j) ⟧ₜ (initialSignatureDCPO Σ) app ρ, and
      ⟦ rhs (inequalities Σ j) ⟧ₜ (initialSignatureDCPO Σ) app ρ
    aren't structurally smaller than
      inequality j ρ

    However, by naturality of ⟦ t ⟧ₜ, they are equal to
      ⟦ lhs (inequalities Σ j) ⟧ₜ (underlyingDCPO A) (interpretation A) (rec ∘ ρ), and
      ⟦ rhs (inequalities Σ j) ⟧ₜ (underlyingDCPO A) (interpretation A) (rec ∘ ρ)
    Here, the recursive call are correct, and the inequality follows immediately,
    as `A` is an algebra. -}
  recIsMonotone (inequality j ρ) =
    subst2 (order (underlyingDCPO A))
      (⟦⟧ₜisNatural (lhs (inequalities Σ j)) (initialSignatureAlgebra Σ) A rec recCommutes ρ)
      (⟦⟧ₜisNatural (rhs (inequalities Σ j)) (initialSignatureAlgebra Σ) A rec recCommutes ρ)
      (inequalityValidity A j (rec ∘ ρ))

  recCommutes c args = refl

  recIsContinuous : isContinuous (initialSignatureDCPO Σ) (underlyingDCPO A) rec
  recIsContinuous I α δ =
    ∐isSup (underlyingDCPO A) (recImageIsDirected δ)

  recContinuousMap : DCPOMorphism (initialSignatureDCPO Σ) (underlyingDCPO A)
  recContinuousMap = scottcontinuousmap rec recIsContinuous

  recMorphism : SignatureMorphism (initialSignatureAlgebra Σ) A
  recMorphism = signaturemorphism recContinuousMap recCommutes

record IndArgs (Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv) (ℓ : Level)
    : Type (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-suc ℓi) ℓc) ℓmb) ℓmc) ℓmct) ℓe) ℓv) (ℓ-suc ℓ)) where
  field
    Y : Initial Σ → Type ℓ
    isPropY : (x : Initial Σ) → isProp (Y x)

    isSupPreservingY : {I : Type ℓi} (α : I → Initial Σ) (δ : isDirected (Leq Σ) α)
                     → ((i : I) → Y (α i))
                     → Y (lub δ)

    isAppPreservingY : (c : constructorNames Σ)
                     → (args : ⟨ ⟦ constructors Σ c ⟧ₘ (initialSignatureDCPO Σ) ⟩)
                     → ⟦ constructors Σ c ⟧ₘᵈᵉᵖ (initialSignatureDCPO Σ) Y args
                     → Y (app c args)

module _ {Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv} {ℓ : Level} (args : IndArgs Σ ℓ) where
  open IndArgs args

  ind : (x : Initial Σ) → Y x
  ind (app c args) =
    {- NOTE: The following two terms are definitionally equal:
             - fmapₘᵈᵉᵖ (constructors Σ c) (initialSignatureDCPO Σ) Y ind args
             - ind ∘ fst args , snd args
             However, the termination checker fails to accept this function if
             we write the former. -}
    isAppPreservingY c args (ind ∘ fst args , snd args)
  ind (lub {α = α} δ) = isSupPreservingY α δ (ind ∘ α)
  ind (leqAntiSym x y x⊑y y⊑x i) =
    isOfHLevel→isOfHLevelDep  isPropY (ind x) (ind y) (leqAntiSym x y x⊑y y⊑x) i
  ind (isSetInitial x y p q i j) =
    isOfHLevel→isOfHLevelDep  (λ y → isProp→isSet (isPropY y))
      (ind x) (ind y) (cong ind p) (cong ind q)
      (isSetInitial x y p q) i j