open import Cubical.Foundations.Prelude hiding (_∧_)

module SignatureAlgebra.Examples.SmashProduct (ℓi : Level) where

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

open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Sigma hiding (_∧_)
open import Cubical.Data.Unit

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

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

open import SignatureAlgebra.Examples.PointedDCPO ℓi

private
  variable
    ℓx ℓa ℓb ℓd ℓt ℓt' ℓt'' : Level

module _ (A : PointedDCPO ℓa ℓt) (B : PointedDCPO ℓb ℓt') where
  data InequalityNames : Type (ℓ-max (ℓ-max (ℓ-max ℓa ℓb) ℓt) ℓt') where
    a⊥⊑⊥b : ⟨ A ⟩ → ⟨ B ⟩ → InequalityNames
    ⊥b⊑a⊥ : ⟨ B ⟩ → ⟨ A ⟩ → InequalityNames

  smashPreΣ : PreSignature ℓ-zero ℓ-zero (ℓ-max ℓa ℓb) (ℓ-max ℓt ℓt')
  smashPreΣ = presignature Unit (λ _ → constantₘ (A ⁻ ×ᵈᶜᵖᵒ B ⁻))

  smashₜ : {V : Type}
         → ⟨ A ⟩
         → ⟨ B ⟩
         → Term smashPreΣ V
  smashₜ a b = constr tt ⊥.rec (a , b)

  smashInequalities : InequalityNames → Inequality smashPreΣ ℓ-zero
  smashInequalities (a⊥⊑⊥b a b) =
    inequality ⊥
      (smashₜ a (least B))
      (smashₜ (least A) b)
  smashInequalities (⊥b⊑a⊥ b a) =
    inequality ⊥
      (smashₜ (least A) b)
      (smashₜ a (least B))

  smashΣ : Signature ℓ-zero ℓ-zero (ℓ-max ℓa ℓb) (ℓ-max ℓt ℓt') (ℓ-max (ℓ-max (ℓ-max ℓa ℓt) ℓb) ℓt') ℓ-zero
  smashΣ = signature smashPreΣ InequalityNames smashInequalities

  SmashAlgebra : (ℓ ℓ' : Level)
               → Type (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-suc ℓi) (ℓ-suc ℓ)) (ℓ-suc ℓ')) (ℓ-max ℓa ℓb)) (ℓ-max ℓt ℓt'))
  SmashAlgebra = SignatureAlgebra smashΣ

  smashalgebra : (D : DCPO ℓd ℓt'')
               → (smash : ⟨ A ⟩ × ⟨ B ⟩ → ⟨ D ⟩)
               → isContinuous (A ⁻ ×ᵈᶜᵖᵒ B ⁻) D smash
               → ((a : ⟨ A ⟩) (b : ⟨ B ⟩) → smash (a , least B) ≡ smash (least A , b))
               → SmashAlgebra ℓd ℓt''
  smashalgebra D smash cont smashEq =
    signaturealgebra
      (presignaturealgebra D
        (λ _ → smash ∘ snd)
        (λ _ →
          isContinuous-∘ (Πᵈᶜᵖᵒ ⊥ (λ _ → D) ×ᵈᶜᵖᵒ (A ⁻ ×ᵈᶜᵖᵒ B ⁻)) (A ⁻ ×ᵈᶜᵖᵒ B ⁻) D
            smash snd cont
            (sndIsContinuous (Πᵈᶜᵖᵒ ⊥ (λ _ → D)) (A ⁻ ×ᵈᶜᵖᵒ B ⁻))))
      λ { (a⊥⊑⊥b a b) ρ → ≡→⊑ D (smashEq a b)
        ; (⊥b⊑a⊥ b a) ρ → ≡→⊑ D (sym (smashEq a b)) }

  initialSmashAlgebra : SmashAlgebra (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-suc ℓi) ℓa) ℓt) ℓb) ℓt') (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-suc ℓi) ℓa) ℓt) ℓb) ℓt')
  initialSmashAlgebra = initialSignatureAlgebra smashΣ

module _ {A : PointedDCPO ℓa ℓt} {B : PointedDCPO ℓb ℓt'} (X : SmashAlgebra A B ℓx ℓt'') where
  smash : ⟨ A ⟩ × ⟨ B ⟩ → ⟨ X ⟩
  smash = interpretation X tt ∘ pairing (const ⊥.rec) (λ x → x)

  smashIsContinuous : isContinuous (A ⁻ ×ᵈᶜᵖᵒ B ⁻) (underlyingDCPO X) smash
  smashIsContinuous =
    isContinuous-∘
      ((A ⁻) ×ᵈᶜᵖᵒ (B ⁻))
      (⟦ constantₘ (A ⁻ ×ᵈᶜᵖᵒ B ⁻) ⟧ₘ (underlyingDCPO X))
      (underlyingDCPO X)
      (interpretation X tt)
      (pairing (const ⊥.rec) (λ x → x))
      (interpretationIsContinuous X tt)
      (pairingIsContinuous
        ((A ⁻) ×ᵈᶜᵖᵒ (B ⁻))
        (Πᵈᶜᵖᵒ ⊥ (λ _ → underlyingDCPO X))
        ((A ⁻) ×ᵈᶜᵖᵒ (B ⁻))
        (const ⊥.rec)
        (λ x → x)
        (constIsContinuous ((A ⁻) ×ᵈᶜᵖᵒ (B ⁻)) (Πᵈᶜᵖᵒ ⊥ (λ _ → underlyingDCPO X)))
        (idIsContinuous ((A ⁻) ×ᵈᶜᵖᵒ (B ⁻))))

  ⟦smashₜ⟧-≡ : {V : Type} {ρ : V → ⟨ X ⟩} {a : ⟨ A ⟩} {b : ⟨ B ⟩}
             → ⟦ smashₜ A B a b ⟧ₜ (underlyingDCPO X) (interpretation X) ρ ≡ smash (a , b)
  ⟦smashₜ⟧-≡ = cong (interpretation X tt) (≡-× (isContr→isProp isContr⊥→A _ _) refl)

  lem : (a : ⟨ A ⟩) (b : ⟨ B ⟩)
      → smash (a , least B) ≡ smash (least A , b)
  lem a b = antisymmetry (underlyingDCPO X) _ _ ⦅1⦆ ⦅2⦆
    where
      ⦅1⦆ : smash (a , least B) ⊑⟨ underlyingDCPO X ⟩ smash (least A , b)
      ⦅1⦆ = subst2 (order (underlyingDCPO X)) ⟦smashₜ⟧-≡ ⟦smashₜ⟧-≡
            (inequalityValidity X (a⊥⊑⊥b a b) ⊥.rec)

      ⦅2⦆ : smash (least A , b) ⊑⟨ underlyingDCPO X ⟩ smash (a , least B)
      ⦅2⦆ = subst2 (order (underlyingDCPO X)) ⟦smashₜ⟧-≡ ⟦smashₜ⟧-≡
            (inequalityValidity X (⊥b⊑a⊥ b a) ⊥.rec)