open import Cubical.Foundations.Prelude

-- We fix a universe level ℓi throughout the development.
-- This level is used for the index types of directed families.
module Paper (ℓi : Level) where

open import Cubical.Categories.Adjoint
open import Cubical.Categories.Category

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

open import Cubical.Data.Bool
open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Nat
open import Cubical.Data.Sigma

open import QIITExamples

open import DCPO ℓi
open import DCPO.Constructions.Unit ℓi

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

private
  variable
    -- Universe levels for monomials
    ℓmb ℓmc ℓmct : Level
    -- Universe levels for DCPOs
    ℓa ℓb ℓd ℓf ℓx ℓt ℓt' ℓt'' : Level
    -- Universe level for variable types
    ℓv : Level
    -- Universe level for constructor names
    ℓc : Level
    -- Universe level for inequality names
    ℓe : Level

-- The QIIT examples from Section 2
FinSet : Type
FinSet = Example1.FinSet

SortedList : Type
SortedList = Example2.SortedList

_≤ₗ_ : ℕ → SortedList → Type
_≤ₗ_ = Example2._≤ₗ_

StrictSortedList : Type
StrictSortedList = Example3.SortedList

_≤ₛ_ : ℕ → StrictSortedList → Type
_≤ₛ_ = Example3._≤ₗ_

-- Section 4: Signatures
-- The running example of the Plotkin powertheory is given at then end of this section
Definition-4-1-Monomial : (ℓmb ℓmc ℓmct : Level)
                        → Type (ℓ-max (ℓ-max (ℓ-max (ℓ-suc ℓi) (ℓ-suc ℓmb)) (ℓ-suc ℓmc)) (ℓ-suc ℓmct))
Definition-4-1-Monomial = Monomial

Definition-4-1-Monomial-Interpretation : (M : Monomial ℓmb ℓmc ℓmct)
                                       → DCPO ℓd ℓt
                                       → DCPO (ℓ-max (ℓ-max ℓmb ℓmc) ℓd) (ℓ-max (ℓ-max ℓmb ℓt) ℓmct)
Definition-4-1-Monomial-Interpretation = ⟦_⟧ₘ

Definition-4-1-Monomial-Interpretation-Fmap : (M : Monomial ℓmb ℓmc ℓmct)
                                            → (D : DCPO ℓd ℓt) (E : DCPO ℓe ℓt')
                                            → (⟨ D ⟩ → ⟨ E ⟩)
                                            → ⟨ ⟦ M ⟧ₘ D ⟩ → ⟨ ⟦ M ⟧ₘ E ⟩
Definition-4-1-Monomial-Interpretation-Fmap = fmapₘ

Definition-4-2-Presignature : (ℓc ℓmb ℓmc ℓmct : Level)
                            → Type (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-suc ℓi) (ℓ-suc ℓc)) (ℓ-suc ℓmb)) (ℓ-suc ℓmc)) (ℓ-suc ℓmct))
Definition-4-2-Presignature = PreSignature

Definition-4-4-Term : (Σ : PreSignature ℓc ℓmb ℓmc ℓmct) (V : Type ℓv)
                    → Type (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-suc ℓi) ℓc) (ℓ-suc ℓmb)) (ℓ-suc ℓmc)) (ℓ-suc ℓmct)) ℓv)
Definition-4-4-Term = Term

Definition-4-5-Inequality : (Σ : PreSignature ℓc ℓmb ℓmc ℓmct) (ℓv : Level)
                          → Type (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-suc ℓi) ℓc) (ℓ-suc ℓmb)) (ℓ-suc ℓmc)) (ℓ-suc ℓmct)) (ℓ-suc ℓv))
Definition-4-5-Inequality = Inequality

Definition-4-6-Signature : (ℓc ℓmb ℓmc ℓmct ℓe ℓv : Level)
                         → Type (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-suc ℓi) (ℓ-suc ℓc)) (ℓ-suc ℓmb)) (ℓ-suc ℓmc)) (ℓ-suc ℓmct)) (ℓ-suc ℓe)) (ℓ-suc ℓv))
Definition-4-6-Signature = Signature

module PlotkinPowerTheory (D : DCPO ℓd ℓt) where
  inclₘ : Monomial ℓ-zero ℓd ℓt
  inclₘ = monomial ⊥ D

  ∪ₘ : Monomial ℓ-zero ℓd ℓt
  ∪ₘ = monomial Bool unitDCPO

  data Name : Type where
    inclName : Name
    unionName : Name

  powerPreΣ : PreSignature ℓ-zero ℓ-zero ℓd ℓt
  powerPreΣ = presignature Name (λ { inclName → inclₘ
                                   ; unionName → ∪ₘ})

  inclₜ : {V : Type} → ⟨ D ⟩ → Term powerPreΣ V
  inclₜ d = constr inclName ⊥.elim d

  _∪ₜ_ : {V : Type} (t₁ t₂ : Term powerPreΣ V) → Term powerPreΣ V
  t₁ ∪ₜ t₂ = constr unionName (if_then t₂ else t₁) tt*

  data InequalityName : Type where
    unionComm : InequalityName
    unionAssoc : InequalityName
    unionIdemp1 : InequalityName
    unionIdemp2 : InequalityName

  data Tri : Type where
    tri1 : Tri
    tri2 : Tri
    tri3 : Tri

  unionInequalities : InequalityName → Inequality powerPreΣ ℓ-zero
  unionInequalities unionComm =
    inequality Bool
      (var false ∪ₜ var true)
      (var true  ∪ₜ var false)
  unionInequalities unionAssoc =
    inequality Tri
      ((var tri1 ∪ₜ var tri2) ∪ₜ var tri3)
      (var tri1 ∪ₜ (var tri2 ∪ₜ var tri3))
  unionInequalities unionIdemp1 =
    inequality Unit
      (var tt ∪ₜ var tt)
      (var tt)
  unionInequalities unionIdemp2 =
    inequality Unit
      (var tt)
      (var tt ∪ₜ var tt)

  powerΣ : Signature ℓ-zero ℓ-zero ℓd ℓt ℓ-zero ℓ-zero
  powerΣ = signature powerPreΣ InequalityName unionInequalities

-- Section 5: Algebras
Definition-5-1-Prealgebra : (Σ : 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)
Definition-5-1-Prealgebra = PreSignatureAlgebra

Definition-5-2-Algebra-Morphism : {Σ : 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)
Definition-5-2-Algebra-Morphism = SignatureMorphism

Definition-5-3-Interpretation : {Σ : PreSignature ℓc ℓmb ℓmc ℓmct} {V : Type ℓv}
                              → Term Σ V
                              → (D : DCPO ℓd ℓt)
                              → ((c : constructorNames Σ) → ⟨ ⟦ constructors Σ c ⟧ₘ D ⟩ → ⟨ D ⟩)
                              → (V → ⟨ D ⟩) → ⟨ D ⟩
Definition-5-3-Interpretation = ⟦_⟧ₜ

Proposition-5-4 : {Σ : 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) ρ)
Proposition-5-4 = ⟦⟧ₜisNatural

Definition-5-5-Valid : {Σ : PreSignature ℓc ℓmb ℓmc ℓmct}
                     → PreSignatureAlgebra Σ ℓa ℓt
                     → Inequality Σ ℓv
                     → Type (ℓ-max (ℓ-max ℓv ℓa) ℓt)
Definition-5-5-Valid = _⊨_

Definition-5-6-Algebra : (Σ : 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)
Definition-5-6-Algebra = SignatureAlgebra

Definition-5-6-Category : (Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv) (ℓ ℓ' : Level)
                        → 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)
Definition-5-6-Category = SignatureAlgebraCategory

-- Section 6: Initial Algebra
Definition-6-1-Initial : (Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv)
                       → Type (initialSignatureAlgebraLevel ℓc ℓmb ℓmc ℓmct ℓe ℓv)
Definition-6-1-Initial = Initial

Definition-6-1-⊑ : (Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv)
                 → Initial Σ → Initial Σ → Type (initialSignatureAlgebraLevel ℓc ℓmb ℓmc ℓmct ℓe ℓv)
Definition-6-1-⊑ = Leq

Lemma-6-3 : (Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv)
          → DCPO (initialSignatureAlgebraLevel ℓc ℓmb ℓmc ℓmct ℓe ℓv)
                  (initialSignatureAlgebraLevel ℓc ℓmb ℓmc ℓmct ℓe ℓv)
Lemma-6-3 = initialSignatureDCPO

Lemma-6-4 : (Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv)
          → PreSignatureAlgebra (preSignature Σ)
              (initialSignatureAlgebraLevel ℓc ℓmb ℓmc ℓmct ℓe ℓv)
              (initialSignatureAlgebraLevel ℓc ℓmb ℓmc ℓmct ℓe ℓv)
Lemma-6-4 Σ = toPreAlgebra (initialSignatureAlgebra Σ)

Lemma-6-5 : (Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv)
          → SignatureAlgebra Σ (initialSignatureAlgebraLevel ℓc ℓmb ℓmc ℓmct ℓe ℓv)
                               (initialSignatureAlgebraLevel ℓc ℓmb ℓmc ℓmct ℓe ℓv)
Lemma-6-5 = initialSignatureAlgebra

Theorem-6-6 : {Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv} (A : SignatureAlgebra Σ ℓa ℓt)
            → Initial Σ → ⟨ A ⟩
Theorem-6-6 = Initial.rec

Definition-6-7-Action : {ℓ : Level} (M : Monomial ℓmb ℓmc ℓmct)
                      → (D : DCPO ℓd ℓt) (Y : ⟨ D ⟩ → Type ℓ)
                      → ⟨ ⟦ M ⟧ₘ D ⟩ → Type (ℓ-max (ℓ-max ℓmb ℓmc) ℓ)
Definition-6-7-Action = ⟦_⟧ₘᵈᵉᵖ

Theorem-6-8 : {Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv} {ℓ : Level}
            → (args : IndArgs Σ ℓ)
            → (x : Initial Σ) → IndArgs.Y args x
Theorem-6-8 = Initial.ind

Theorem-6-9 : {Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv}
            → (A : SignatureAlgebra Σ ℓa ℓt)
            → isContr (SignatureMorphism (initialSignatureAlgebra Σ) A)
Theorem-6-9 = initiality

-- Section 7: Examples
-- 7.1 Coalesced Sum
open import SignatureAlgebra.Examples.CoalescedSum ℓi
-- 7.2 Coequalizer
open import SignatureAlgebra.Examples.Coequalizer ℓi
-- 7.3 Smash Product
open import SignatureAlgebra.Examples.SmashProduct ℓi

Definition-7-7 : (Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv)
               → (D : DCPO ℓd ℓt)
               → Signature ℓc ℓmb (ℓ-max ℓd ℓmc) (ℓ-max ℓt ℓmct) ℓe ℓv
Definition-7-7 = _+ˢⁱᵍ_

_+ᵃˡᵍ_ : {Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv} {D : DCPO ℓd ℓt} {ℓ ℓ' : Level}
       → (X : SignatureAlgebra Σ ℓ ℓ')
       → DCPOMorphism D (underlyingDCPO X)
       → SignatureAlgebra (Σ +ˢⁱᵍ D) ℓ ℓ'
_+ᵃˡᵍ_ = addIncl

_⁻ᵃˡᵍ : {Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv} {D : DCPO ℓd ℓt} {ℓ ℓ' : Level}
      → SignatureAlgebra (Σ +ˢⁱᵍ D) ℓ ℓ'
      → SignatureAlgebra Σ ℓ ℓ'
_⁻ᵃˡᵍ = forgetIncl

open UnitCounit

Theorem-7-8 : (Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv)
            → Free Σ ⊣ Underlying Σ
Theorem-7-8 = Free⊣Underlying

-- 7.5: Pointed DCPO
open import SignatureAlgebra.Examples.PointedDCPO ℓi
-- 7.5: Power Algebras
open import SignatureAlgebra.Examples.PowerDomain ℓi