open import Cubical.Foundations.Prelude

module SignatureAlgebra.SignatureAlgebraOver (ℓi : Level) where

open import Cubical.Categories.Category

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

open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Sigma
open import Cubical.Data.Sum as ⊎
open import Cubical.Data.Unit

open import DCPO ℓi
open import DCPO.Constructions.BinaryProduct ℓi
open import DCPO.Constructions.Lift ℓi
open import DCPO.Constructions.Product ℓi

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

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

liftMonomial : (ℓmb' ℓmc' ℓmct' : Level)
             → (M : Monomial ℓmb ℓmc ℓmct)
             → Monomial (ℓ-max ℓmb ℓmb') (ℓ-max ℓmc ℓmc') (ℓ-max ℓmct ℓmct')
liftMonomial ℓmb' ℓmc' ℓmct' (monomial B C) =
  monomial (Lift {j = ℓmb'} B) (liftDCPO ℓmc' ℓmct' C)

lowerArgs : (ℓmb' ℓmc' ℓmct' : Level)
          → (M : Monomial ℓmb ℓmc ℓmct) (D : DCPO ℓd ℓt)
          → ⟨ ⟦ liftMonomial ℓmb' ℓmc' ℓmct' M ⟧ₘ D ⟩
          → ⟨ ⟦ M ⟧ₘ D ⟩
lowerArgs _ _ _ P D = pairing ((_∘ lift) ∘ fst) (lower ∘ snd)

liftArgs : (ℓmb' ℓmc' ℓmct' : Level)
         → (M : Monomial ℓmb ℓmc ℓmct) (D : DCPO ℓd ℓt)
         → ⟨ ⟦ M ⟧ₘ D ⟩
         → ⟨ ⟦ liftMonomial ℓmb' ℓmc' ℓmct' M ⟧ₘ D ⟩
liftArgs _ _ _ P D = pairing ((_∘ lower) ∘ fst) (lift ∘ snd)

lowerArgsIsContinuous : {ℓmb' ℓmc' ℓmct' : Level}
                      → (M : Monomial ℓmb ℓmc ℓmct) (D : DCPO ℓd ℓt)
                      → isContinuous (⟦ liftMonomial ℓmb' ℓmc' ℓmct' M ⟧ₘ D) (⟦ M ⟧ₘ D)
                        (lowerArgs ℓmb' ℓmc' ℓmct' M D)
lowerArgsIsContinuous M@(monomial B C) D =
  pairingIsContinuous (⟦ liftMonomial _ _ _ M ⟧ₘ D) (Πᵈᶜᵖᵒ B (λ _ → D)) C
    ((_∘ lift) ∘ fst)
    (lower ∘ snd)
    (isContinuous-∘ (⟦ liftMonomial _ _ _ M ⟧ₘ D) (Πᵈᶜᵖᵒ (Lift B) (λ _ → D)) (Πᵈᶜᵖᵒ B (λ _ → D))
      (_∘ lift) fst
      (λ I α δ →
        (λ i b → ∐isUpperbound D (pointwiseFamilyIsDirected' (Lift B) (λ _ → D) δ (lift b)) i) ,
        λ v vIsUpper b → ∐isLowerBoundOfUpperbounds D (pointwiseFamilyIsDirected' (Lift B) (λ _ → D) δ (lift b)) (v b) (λ i → vIsUpper i b))
      (fstIsContinuous (Πᵈᶜᵖᵒ (Lift B) (λ _ → D)) (liftDCPO _ _ C)))
    (isContinuous-∘ (⟦ liftMonomial _ _ _ M ⟧ₘ D) (liftDCPO _ _ C) C
      lower snd
      (lowerIsContinuous _ _ C)
      (sndIsContinuous (Πᵈᶜᵖᵒ (Lift B) (λ _ → D)) (liftDCPO _ _ C)))

liftArgsIsContinuous : {ℓmb' ℓmc' ℓmct' : Level}
                     → (M : Monomial ℓmb ℓmc ℓmct) (D : DCPO ℓd ℓt)
                     → isContinuous (⟦ M ⟧ₘ D) (⟦ liftMonomial ℓmb' ℓmc' ℓmct' M ⟧ₘ D)
                        (liftArgs ℓmb' ℓmc' ℓmct' M D)
liftArgsIsContinuous M@(monomial B C) D =
  pairingIsContinuous (⟦ M ⟧ₘ D) (Πᵈᶜᵖᵒ (Lift B) (λ _ → D)) (liftDCPO _ _ C)
    ((_∘ lower) ∘ fst)
    (lift ∘ snd)
    (isContinuous-∘ (⟦ M ⟧ₘ D) (Πᵈᶜᵖᵒ B (λ _ → D)) (Πᵈᶜᵖᵒ (Lift B) (λ _ → D))
      (_∘ lower) fst
      (λ I α δ →
        (λ i b → ∐isUpperbound D (pointwiseFamilyIsDirected' B (λ _ → D) δ (lower b)) i) ,
        λ v vIsUpper b → ∐isLowerBoundOfUpperbounds D (pointwiseFamilyIsDirected' B (λ _ → D) δ (lower b)) (v b) (λ i → vIsUpper i b))
      (fstIsContinuous (Πᵈᶜᵖᵒ B (λ _ → D)) C))
    (isContinuous-∘ (⟦ M ⟧ₘ D) C (liftDCPO _ _ C)
      lift snd
      (liftIsContinuous _ _ C)
      (sndIsContinuous (Πᵈᶜᵖᵒ B (λ _ → D)) C))

module _ {ℓd ℓt ℓmb ℓmc ℓmct : Level} where
  _+ᵖʳᵉˢⁱᵍ_ : (Σ : PreSignature ℓc ℓmb ℓmc ℓmct)
            → (D : DCPO ℓd ℓt)
            → PreSignature ℓc ℓmb (ℓ-max ℓd ℓmc) (ℓ-max ℓt ℓmct)
  Σ +ᵖʳᵉˢⁱᵍ D =
    presignature (constructorNames Σ ⊎ Unit)
      (⊎.rec (liftMonomial ℓ-zero ℓd ℓt ∘ constructors Σ)
              (λ _ → liftMonomial ℓmb ℓmc ℓmct (constantₘ D)))

termOver : {V : Type ℓv}
         → (Σ : PreSignature ℓc ℓmb ℓmc ℓmct)
         → (D : DCPO ℓd ℓt)
         → Term Σ V
         → Term (Σ +ᵖʳᵉˢⁱᵍ D) V
termOver Σ D (var x) = var x
termOver Σ D (constr cName f c) =
  constr (inl cName) (termOver Σ D ∘ f ∘ lower) (lift c)

inequalityOver : (Σ : PreSignature ℓc ℓmb ℓmc ℓmct)
               → (D : DCPO ℓd ℓt)
               → Inequality Σ ℓv
               → Inequality (Σ +ᵖʳᵉˢⁱᵍ D) ℓv
inequalityOver Σ D (inequality V lhs rhs) =
  inequality V (termOver Σ D lhs) (termOver Σ D rhs)

_+ˢⁱᵍ_ : (Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv)
       → (D : DCPO ℓd ℓt)
       → Signature ℓc ℓmb (ℓ-max ℓd ℓmc) (ℓ-max ℓt ℓmct) ℓe ℓv
Σ +ˢⁱᵍ D =
  signature
    (preSignature Σ +ᵖʳᵉˢⁱᵍ D)
    (inequalityNames Σ)
    (inequalityOver (preSignature Σ) D ∘ inequalities Σ)

module _ {Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv} {D : DCPO ℓd ℓt} {ℓ ℓ' : Level} where

  forgetIncl : SignatureAlgebra (Σ +ˢⁱᵍ D) ℓ ℓ'
             → SignatureAlgebra Σ ℓ ℓ'
  forgetIncl X =
    signaturealgebra
      (presignaturealgebra
        (underlyingDCPO X)
        interpWithoutIncl
        interpWithoutInclIsContinuous)
      (λ j ρ →
        subst2 (order (underlyingDCPO X))
          (lem (lhs (inequalities Σ j)) ρ)
          (lem (rhs (inequalities Σ j)) ρ)
          (inequalityValidity X j ρ))
    where
      interpWithoutIncl : (c : constructorNames Σ)
                        → ⟨ ⟦ constructors Σ c ⟧ₘ (underlyingDCPO X) ⟩
                        → ⟨ X ⟩
      interpWithoutIncl c = interpretation X (inl c) ∘
                            liftArgs ℓ-zero ℓd ℓt (constructors Σ c) (underlyingDCPO X)

      abstract
        interpWithoutInclIsContinuous : (c : constructorNames Σ)
                                      → isContinuous
                                          (⟦ constructors Σ c ⟧ₘ (underlyingDCPO X))
                                          (underlyingDCPO X)
                                          (interpWithoutIncl c)
        interpWithoutInclIsContinuous c =
          isContinuous-∘
            (⟦ constructors Σ c ⟧ₘ (underlyingDCPO X))
            (⟦ constructors (Σ +ˢⁱᵍ D) (inl c) ⟧ₘ (underlyingDCPO X))
            (underlyingDCPO X)
            (interpretation X (inl c))
            (liftArgs ℓ-zero ℓd ℓt (constructors Σ c) (underlyingDCPO X))
            (interpretationIsContinuous X (inl c))
            (liftArgsIsContinuous (constructors Σ c) (underlyingDCPO X))

      lem : {V : Type ℓv} (t : Term (preSignature Σ) V) (ρ : V → ⟨ X ⟩)
          → ⟦ termOver (preSignature Σ) D t ⟧ₜ (underlyingDCPO X) (interpretation X) ρ
          ≡ ⟦ t ⟧ₜ (underlyingDCPO X) interpWithoutIncl ρ
      lem (var x) ρ = refl
      lem (constr cName f c) ρ =
        cong (interpretation X (inl cName))
          (≡-× (funExt (λ b → lem (f (lower b)) ρ)) refl)

  addIncl : (X : SignatureAlgebra Σ ℓ ℓ')
          → DCPOMorphism D (underlyingDCPO X)
          → SignatureAlgebra (Σ +ˢⁱᵍ D) ℓ ℓ'
  addIncl X f =
    signaturealgebra
      (presignaturealgebra (underlyingDCPO X) interp interpIsContinuous)
      (λ j ρ →
        subst2 (order (underlyingDCPO X))
          (lem (lhs (inequalities Σ j)) ρ)
          (lem (rhs (inequalities Σ j)) ρ)
          (inequalityValidity X j ρ))
    where
      interp : (c : constructorNames Σ ⊎ Unit)
              → ⟨ ⟦ constructors (Σ +ˢⁱᵍ D) c ⟧ₘ (underlyingDCPO X) ⟩
              → ⟨ X ⟩
      interp (inl c) = interpretation X c ∘ lowerArgs ℓ-zero ℓd ℓt (constructors Σ c) (underlyingDCPO X)
      interp (inr tt) = function f ∘ lower ∘ snd

      abstract
        interpIsContinuous : (c : constructorNames Σ ⊎ Unit)
                          → isContinuous
                              (⟦ constructors (Σ +ˢⁱᵍ D) c ⟧ₘ (underlyingDCPO X))
                              (underlyingDCPO X)
                              (interp c)
        interpIsContinuous (inl c) =
          isContinuous-∘
          (⟦ liftMonomial ℓ-zero ℓd ℓt (constructors Σ c) ⟧ₘ (underlyingDCPO X))
          (⟦ constructors Σ c ⟧ₘ (underlyingDCPO X))
          (underlyingDCPO X)
          (interpretation X c)
          (lowerArgs ℓ-zero ℓd ℓt (constructors Σ c) (underlyingDCPO X))
          (interpretationIsContinuous X c)
          (lowerArgsIsContinuous (constructors Σ c) (underlyingDCPO X))
        interpIsContinuous (inr tt) =
          isContinuous-∘
            (⟦ liftMonomial ℓmb ℓmc ℓmct (constantₘ D) ⟧ₘ (underlyingDCPO X))
            (liftDCPO ℓmc ℓmct D)
            (underlyingDCPO X)
            (function f ∘ lower)
            snd
            (isContinuous-∘
              (liftDCPO ℓmc ℓmct D)
              D
              (underlyingDCPO X)
              (function f)
              lower
              (continuity f)
              (lowerIsContinuous _ _ D))
            (sndIsContinuous (Πᵈᶜᵖᵒ ⊥* (λ _ → underlyingDCPO X)) (liftDCPO ℓmc ℓmct D))

      lem : {V : Type ℓv} (t : Term (preSignature Σ) V) (ρ : V → ⟨ X ⟩)
          → ⟦ t ⟧ₜ (underlyingDCPO X) (interpretation X) ρ
          ≡ ⟦ termOver (preSignature Σ) D t ⟧ₜ (underlyingDCPO X) interp ρ
      lem (var x) ρ = refl
      lem (constr cName f c) ρ =
        cong (interpretation X cName) (≡-× (funExt (λ b → lem (f b) ρ)) refl)

  incl : (X : SignatureAlgebra (Σ +ˢⁱᵍ D) ℓ ℓ')
       → ⟨ D ⟩ → ⟨ X ⟩
  incl X = interpretation X (inr tt) ∘ pairing (const ⊥.rec*) lift

  abstract
    inclIsContinuous : (X : SignatureAlgebra (Σ +ˢⁱᵍ D) ℓ ℓ')
                    → isContinuous D (underlyingDCPO X) (incl X)
    inclIsContinuous X =
      isContinuous-∘
        D
        (Πᵈᶜᵖᵒ ⊥* (λ _ → underlyingDCPO X) ×ᵈᶜᵖᵒ liftDCPO ℓmc ℓmct D)
        (underlyingDCPO X)
        (interpretation X (inr tt))
        (pairing (const ⊥.rec*) lift)
        (interpretationIsContinuous X (inr tt))
        (pairingIsContinuous
          D (Πᵈᶜᵖᵒ ⊥* (λ _ → underlyingDCPO X)) (liftDCPO ℓmc ℓmct D)
          (const rec*) lift
          (constIsContinuous D (Πᵈᶜᵖᵒ ⊥* (λ _ → underlyingDCPO X)))
          (liftIsContinuous _ _ D))

  inclContinuousMap : (X : SignatureAlgebra (Σ +ˢⁱᵍ D) ℓ ℓ')
                    → DCPOMorphism D (underlyingDCPO X)
  inclContinuousMap X = scottcontinuousmap (incl X) (inclIsContinuous X)