open import Cubical.Foundations.Prelude

module SignatureAlgebra.SignatureAlgebra (ℓi : Level) where

open import Cubical.Categories.Category

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

open import Cubical.Data.Sigma

open import Cubical.Reflection.RecordEquiv

open import DCPO ℓi

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

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

record PreSignatureAlgebraStr
      (Σ : PreSignature ℓc ℓmb ℓmc ℓmct)
      (ℓt : Level)
      (A : Type ℓa)
    : Type (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-suc ℓi) ℓa) (ℓ-suc ℓt)) ℓc) ℓmb) ℓmc) ℓmct) where
  constructor presignaturealgebrastr
  field
    dcpoStr : DCPOStr ℓa ℓt A
    interpretation : (c : constructorNames Σ) → DCPOMorphism (⟦ constructors Σ c ⟧ₘ (A , dcpoStr)) (A , dcpoStr)

PreSignatureAlgebra : (Σ : PreSignature ℓc ℓmb ℓmc ℓmct) (ℓa ℓt : Level)
                    → Type (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-suc ℓi) (ℓ-suc ℓa)) (ℓ-suc ℓt)) ℓc) ℓmb) ℓmc) ℓmct)
PreSignatureAlgebra Σ ℓa ℓt = TypeWithStr ℓa (PreSignatureAlgebraStr Σ ℓt)

presignaturealgebra : {Σ : PreSignature ℓc ℓmb ℓmc ℓmct}
                    → (D : DCPO ℓa ℓt)
                    → (interpretation : (c : constructorNames Σ) → ⟨ ⟦ constructors Σ c ⟧ₘ D ⟩ → ⟨ D ⟩)
                    → ((c : constructorNames Σ)
                        → isContinuous (⟦ constructors Σ c ⟧ₘ D)
                                       D
                                       (interpretation c))
                    → PreSignatureAlgebra Σ ℓa ℓt
presignaturealgebra D interpretation interpretationIsContinuous =
  ⟨ D ⟩ , presignaturealgebrastr (str D) (λ c → scottcontinuousmap (interpretation c) (interpretationIsContinuous c))

underlyingDCPOₚᵣₑ : {Σ : PreSignature ℓc ℓmb ℓmc ℓmct}
                  → PreSignatureAlgebra Σ ℓa ℓt
                  → DCPO ℓa ℓt
underlyingDCPOₚᵣₑ A = ⟨ A ⟩ , PreSignatureAlgebraStr.dcpoStr (str A)

interpretationₚᵣₑ : {Σ : PreSignature ℓc ℓmb ℓmc ℓmct}
                  → (A : PreSignatureAlgebra Σ ℓa ℓt)
                  → (c : constructorNames Σ)
                  → ⟨ ⟦ constructors Σ c ⟧ₘ (underlyingDCPOₚᵣₑ A) ⟩ → ⟨ A ⟩
interpretationₚᵣₑ A c = function (PreSignatureAlgebraStr.interpretation (str A) c)

interpretationIsContinuousₚᵣₑ : {Σ : PreSignature ℓc ℓmb ℓmc ℓmct}
                              → (A : PreSignatureAlgebra Σ ℓa ℓt)
                              → (c : constructorNames Σ)
                              → isContinuous (⟦ constructors Σ c ⟧ₘ (underlyingDCPOₚᵣₑ A))
                                             (underlyingDCPOₚᵣₑ A)
                                             (interpretationₚᵣₑ A c)
interpretationIsContinuousₚᵣₑ A c = continuity (PreSignatureAlgebraStr.interpretation (str A) c)

_⊨_ : {Σ : PreSignature ℓc ℓmb ℓmc ℓmct}
    → PreSignatureAlgebra Σ ℓa ℓt
    → Inequality Σ ℓv
    → Type (ℓ-max (ℓ-max ℓv ℓa) ℓt)
A ⊨ ineq =
    (ρ : V ineq → ⟨ D ⟩)
  → ⟦ lhs ineq ⟧ₜ D (interpretationₚᵣₑ A) ρ
      ⊑⟨ D ⟩
    ⟦ rhs ineq ⟧ₜ D (interpretationₚᵣₑ A) ρ
  where
    D = underlyingDCPOₚᵣₑ A

record SignatureAlgebraStr
      (Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv)
      (ℓt : Level)
      (A : Type ℓa)
    : Type (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-suc ℓi) ℓa) (ℓ-suc ℓt)) ℓc) ℓmb) ℓmc) ℓmct) ℓe) ℓv) where
  constructor signaturealgebrastr
  field
    preStr : PreSignatureAlgebraStr (preSignature Σ) ℓt A
    inequalityValidity : (j : inequalityNames Σ)
                       → (A , preStr) ⊨ inequalities Σ j

SignatureAlgebra : (Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv) (ℓa ℓt : Level)
                 → Type (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-suc ℓi) (ℓ-suc ℓa)) (ℓ-suc ℓt)) ℓc) ℓmb) ℓmc) ℓmct) ℓe) ℓv)
SignatureAlgebra Σ ℓa ℓt = TypeWithStr ℓa (SignatureAlgebraStr Σ ℓt)

signaturealgebra : {Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv}
                 → (A : PreSignatureAlgebra (preSignature Σ) ℓa ℓt)
                 → ((j : inequalityNames Σ) → A ⊨ inequalities Σ j)
                 → SignatureAlgebra Σ ℓa ℓt
signaturealgebra A inequalityValidity = ⟨ A ⟩ , signaturealgebrastr (str A) inequalityValidity

toPreAlgebra : {Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv}
             → SignatureAlgebra Σ ℓa ℓt
             → PreSignatureAlgebra (preSignature Σ) ℓa ℓt
toPreAlgebra A = ⟨ A ⟩ , SignatureAlgebraStr.preStr (str A)

underlyingDCPO : {Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv}
               → SignatureAlgebra Σ ℓa ℓt
               → DCPO ℓa ℓt
underlyingDCPO A = underlyingDCPOₚᵣₑ (toPreAlgebra A)

algebraOrder : {Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv}
             → (A : SignatureAlgebra Σ ℓa ℓt)
             → ⟨ A ⟩ → ⟨ A ⟩ → Type ℓt
algebraOrder A = order (underlyingDCPO A)

interpretation : {Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv}
               → (A : SignatureAlgebra Σ ℓa ℓt)
               → (c : constructorNames Σ)
               → ⟨ ⟦ constructors Σ c ⟧ₘ (underlyingDCPO A) ⟩ → ⟨ A ⟩
interpretation A = interpretationₚᵣₑ (toPreAlgebra A)

interpretationIsContinuous : {Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv}
                           → (A : SignatureAlgebra Σ ℓa ℓt)
                           → (c : constructorNames Σ)
                           → isContinuous (⟦ constructors Σ c ⟧ₘ (underlyingDCPO A))
                                          (underlyingDCPO A)
                                          (interpretation A c)
interpretationIsContinuous A = interpretationIsContinuousₚᵣₑ (toPreAlgebra A)

inequalityValidity : {Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv}
                   → (A : SignatureAlgebra Σ ℓa ℓt)
                   → (j : inequalityNames Σ)
                   → toPreAlgebra A ⊨ inequalities Σ j
inequalityValidity A = SignatureAlgebraStr.inequalityValidity (str A)

isCommutingWithInterpretation : {Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv}
                              → (A : SignatureAlgebra Σ ℓa ℓt) (B : SignatureAlgebra Σ ℓb ℓt')
                              → (f : ⟨ A ⟩ → ⟨ B ⟩)
                              → Type (ℓ-max (ℓ-max (ℓ-max (ℓ-max ℓc ℓmb) ℓmc) ℓa) ℓb)
isCommutingWithInterpretation {Σ = Σ} A B f =
    (c : constructorNames Σ)
  → (x : ⟨ ⟦ constructors Σ c ⟧ₘ (underlyingDCPO A) ⟩)
  → interpretation B c (fmapₘ (constructors Σ c) (underlyingDCPO A) (underlyingDCPO B) f x)
  ≡ f (interpretation A c x)

isPropIsCommutingWithInterpretation : {Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv}
                                    → (A : SignatureAlgebra Σ ℓa ℓt) (B : SignatureAlgebra Σ ℓb ℓt')
                                    → (f : ⟨ A ⟩ → ⟨ B ⟩)
                                    → isProp (isCommutingWithInterpretation A B f)
isPropIsCommutingWithInterpretation A B f =
  isPropΠ2 (λ _ _ → sethood (underlyingDCPO B) _ _)

record SignatureMorphism
    {Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv}
    (A : SignatureAlgebra Σ ℓa ℓt) (B : SignatureAlgebra Σ ℓb ℓt')
    : Type (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-suc ℓi) ℓa) ℓb) ℓt) ℓt') ℓc) ℓmb) ℓmc) where
  constructor signaturemorphism
  field
    continuousMap : DCPOMorphism (underlyingDCPO A) (underlyingDCPO B)
    commutation : isCommutingWithInterpretation A B (function continuousMap)

  open DCPOMorphism continuousMap using (function) public
open SignatureMorphism public

unquoteDecl SignatureMorphismIsoΣ = declareRecordIsoΣ SignatureMorphismIsoΣ (quote SignatureMorphism)

module _ {Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv}
         {A : SignatureAlgebra Σ ℓa ℓt} {B : SignatureAlgebra Σ ℓb ℓt'} where

  SignatureMorphism≡' : {f g : SignatureMorphism A B}
                      → continuousMap f ≡ continuousMap g
                      → f ≡ g
  SignatureMorphism≡' {f = f} {g = g} p =
    isoFunInjective SignatureMorphismIsoΣ f g
      (Σ≡Prop (λ h → isPropIsCommutingWithInterpretation A B (function h)) p)

  SignatureMorphism≡ : {f g : SignatureMorphism A B}
                     → function f ≡ function g
                     → f ≡ g
  SignatureMorphism≡ p = SignatureMorphism≡' (DCPOMorphism≡ p)

  isSetSignatureMorphism : isSet (SignatureMorphism A B)
  isSetSignatureMorphism =
    isOfHLevelRetractFromIso  SignatureMorphismIsoΣ
      (isSetΣ isSetDCPOMorphism λ f → isProp→isSet (isPropIsCommutingWithInterpretation A B (function f)))

⟦⟧ₜisNatural : {Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv} {V : Type ℓv}
             → (t : Term (preSignature Σ) V)
             → (A : SignatureAlgebra Σ ℓa ℓt) (B : SignatureAlgebra Σ ℓb ℓt')
             → (f : ⟨ A ⟩ → ⟨ B ⟩)
             → isCommutingWithInterpretation A B f
             → (ρ : (V → ⟨ A ⟩))
             → ⟦ t ⟧ₜ (underlyingDCPO B) (interpretation B) (f ∘ ρ)
             ≡ f (⟦ t ⟧ₜ (underlyingDCPO A) (interpretation A) ρ)
⟦⟧ₜisNatural (var x) A B f fCommutes ρ = refl
⟦⟧ₜisNatural {Σ = Σ} (constr cName g c) A B f fCommutes ρ =
  ⟦ constr cName g c ⟧ₜ (underlyingDCPO B) (interpretation B) (f ∘ ρ)                       ≡⟨ refl ⟩
  interpretation B cName
    ((λ b → ⟦ g b ⟧ₜ (underlyingDCPO B) (interpretation B) (f ∘ ρ)) , c)                    ≡⟨ cong (interpretation B cName) (≡-× (funExt (λ b → ⟦⟧ₜisNatural (g b) A B f fCommutes ρ)) refl) ⟩
  interpretation B cName
    (fmapₘ (constructors Σ cName)
      (underlyingDCPO A) (underlyingDCPO B) f
      ((λ b → ⟦ g b ⟧ₜ (underlyingDCPO A) (interpretation A) ρ) , c))                       ≡⟨ fCommutes cName _ ⟩
  f (interpretation A cName ((λ b → ⟦ g b ⟧ₜ (underlyingDCPO A) (interpretation A) ρ) , c)) ≡⟨ refl ⟩
  f (⟦ constr cName g c ⟧ₜ (underlyingDCPO A) (interpretation A) ρ) ∎

idˢⁱᵍ : {Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv} {A : SignatureAlgebra Σ ℓa ℓt}
      → SignatureMorphism A A
idˢⁱᵍ = signaturemorphism idᵈᶜᵖᵒ λ _ _ → refl

infixr  _∘ˢⁱᵍ_
_∘ˢⁱᵍ_ : {Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv}
         {A : SignatureAlgebra Σ ℓa ℓt} {B : SignatureAlgebra Σ ℓb ℓt'}
         {ℓ ℓ' : Level} {C : SignatureAlgebra Σ ℓ ℓ'}
       → SignatureMorphism B C
       → SignatureMorphism A B
       → SignatureMorphism A C
g ∘ˢⁱᵍ f =
  signaturemorphism (continuousMap g ∘ᵈᶜᵖᵒ continuousMap f)
    λ c args → commutation g c _ ∙ cong (function g) (commutation f c args)

module _ (Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv) (ℓ ℓ' : Level) where
  open Category

  SignatureAlgebraCategory : Category (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-suc ℓi) (ℓ-suc ℓ)) (ℓ-suc ℓ')) ℓc) ℓmb) ℓmc) ℓmct) ℓe) ℓv) (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-suc ℓi) ℓ) ℓ') ℓc) ℓmb) ℓmc)
  SignatureAlgebraCategory .ob = SignatureAlgebra Σ ℓ ℓ'
  SignatureAlgebraCategory .Hom[_,_] = SignatureMorphism
  SignatureAlgebraCategory .id = idˢⁱᵍ
  SignatureAlgebraCategory ._⋆_ f g = g ∘ˢⁱᵍ f
  SignatureAlgebraCategory .⋆IdL f = SignatureMorphism≡ refl
  SignatureAlgebraCategory .⋆IdR f = SignatureMorphism≡ refl
  SignatureAlgebraCategory .⋆Assoc f g h = SignatureMorphism≡ refl
  SignatureAlgebraCategory .isSetHom = isSetSignatureMorphism