open import Cubical.Foundations.Prelude

module SignatureAlgebra.Monomial (ℓi : Level) where

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

open import Cubical.Data.Empty
open import Cubical.Data.Sigma

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

private
  variable
    ℓ ℓd ℓe ℓt ℓt' ℓmb ℓmc ℓmct : Level

record Monomial (ℓmb ℓmc ℓmct : Level) : Type (ℓ-max (ℓ-max (ℓ-max (ℓ-suc ℓi) (ℓ-suc ℓmb)) (ℓ-suc ℓmc)) (ℓ-suc ℓmct)) where
  constructor monomial
  field
    B : Type ℓmb
    C : DCPO ℓmc ℓmct

constantₘ : (D : DCPO ℓd ℓt) → Monomial ℓ-zero ℓd ℓt
constantₘ D = monomial ⊥ D

⟦_⟧ₘ : (M : Monomial ℓmb ℓmc ℓmct)
      → DCPO ℓd ℓt
      → DCPO (ℓ-max (ℓ-max ℓmb ℓmc) ℓd) (ℓ-max (ℓ-max ℓmb ℓt) ℓmct)
⟦ monomial B C ⟧ₘ X = (Πᵈᶜᵖᵒ B (λ _ → X)) ×ᵈᶜᵖᵒ C

fmapₘ : (M : Monomial ℓmb ℓmc ℓmct) (D : DCPO ℓd ℓt) (E : DCPO ℓe ℓt')
      → (⟨ D ⟩ → ⟨ E ⟩)
      → ⟨ ⟦ M ⟧ₘ D ⟩ → ⟨ ⟦ M ⟧ₘ E ⟩
fmapₘ (monomial B C) D E f x = f ∘ fst x , snd x

fmapₘ≡ : (M : Monomial ℓmb ℓmc ℓmct) (D : DCPO ℓd ℓt) (E : DCPO ℓe ℓt')
       → (f g : ⟨ D ⟩ → ⟨ E ⟩) {args : ⟨ ⟦ M ⟧ₘ D ⟩}
       → f ∘ fst args ≡ g ∘ fst args
       → fmapₘ M D E f args ≡ fmapₘ M D E g args
fmapₘ≡ M D E f g {args} p = ≡-× p refl

fmapₘisMonotone : (M : Monomial ℓmb ℓmc ℓmct) (D : DCPO ℓd ℓt) (E : DCPO ℓe ℓt')
                → (f : ⟨ D ⟩ → ⟨ E ⟩)
                → isMonotone D E f
                → isMonotone (⟦ M ⟧ₘ D) (⟦ M ⟧ₘ E) (fmapₘ M D E f)
fmapₘisMonotone (monomial B C) D E f fMono {g₁ , c₁} {g₂ , c₂} (g₁⊑g₂ , c₁⊑c₂) =
  (λ b → fMono (g₁⊑g₂ b)) , c₁⊑c₂

{- NOTE: We could we made Y : ⟨ D ⟩ → DCPO, such that ⟦ M ⟧ₘᵈᵉᵖ D Y z : DCPO,
         but we currently do not need this anywhere, so it would only complicate
         stuff -}
⟦_⟧ₘᵈᵉᵖ : (M : Monomial ℓmb ℓmc ℓmct) (D : DCPO ℓd ℓt) (Y : ⟨ D ⟩ → Type ℓ)
        → ⟨ ⟦ M ⟧ₘ D ⟩ → Type (ℓ-max (ℓ-max ℓmb ℓmc) ℓ)
⟦ monomial B C ⟧ₘᵈᵉᵖ D Y z = ((b : B) → Y (fst z b)) × ⟨ C ⟩

fmapₘᵈᵉᵖ : (M : Monomial ℓmb ℓmc ℓmct) (D : DCPO ℓd ℓt) (Y : ⟨ D ⟩ → Type ℓ)
         → ((x : ⟨ D ⟩) → Y x )
         → (x : ⟨ ⟦ M ⟧ₘ D ⟩) → ⟦ M ⟧ₘᵈᵉᵖ D Y x
fmapₘᵈᵉᵖ (monomial B C) D Y f z = f ∘ fst z , snd z