    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Example of multi-sorted algebras as indexed containers
    ------------------------------------------------------------------------

    {-# OPTIONS --safe --cubical-compatible #-}

    module README.Data.Container.Indexed.MultiSortedAlgebraExample where

    ------------------------------------------------------------------------
    -- Preliminaries
    ------------------------------------------------------------------------
    -- We import library content for indexed containers, standard types,
    -- and setoids.

    open import Level

    open import Data.Container.Indexed.Core using (Container; ⟦_⟧; _◃_/_)
    open import Data.Container.Indexed.FreeMonad using (_⋆C_)
    open import Data.W.Indexed using (W; sup)

    open import Data.Product using (Σ; _×_; _,_; Σ-syntax)
    open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_])
    open import Data.Empty.Polymorphic using (⊥; ⊥-elim)

    open import Function using (_∘_)
    open import Function.Bundles using (Func)

    open import Relation.Binary using (Setoid; IsEquivalence)
    open import Relation.Binary.PropositionalEquality using (_≡_; refl)

    import Data.Container.Indexed.Relation.Binary.Equality.Setoid as ICSetoid
    import Relation.Binary.Reasoning.Setoid as SetoidReasoning

    open Setoid using (Carrier; _≈_; isEquivalence)
    open Func renaming (to to apply)

    -- Letter ℓ denotes universe levels.

    variable
      ℓ ℓ' ℓˢ ℓᵒ ℓᵃ ℓᵐ ℓᵉ ℓⁱ : Level
      I : Set ℓⁱ
      S : Set ℓˢ

    ------------------------------------------------------------------------
    -- The interpretation of a container (Op ◃ Ar / sort) is
    --
    --   ⟦ Op ◃ Ar / sort ⟧ X s = Σ[ o ∈ Op s ] ((i : Ar o) → X (sort o i))
    --
    -- which contains pairs consisting of an operator $o$ and its collection
    -- of arguments.  The least fixed point of (X ↦ ⟦ C ⟧ X) is the indexed
    -- W-type given by C, and it contains closed first-order terms of the
    -- multi-sorted algebra C.

    -- We need to interpret indexed containers on Setoids.
    -- This definition is missing from the standard library v1.7.

    ⟦_⟧s : (C : Container I S ℓᵒ ℓᵃ) (ξ : I → Setoid ℓᵐ ℓᵉ) → S → Setoid _ _
    ⟦ C ⟧s ξ = ICSetoid.setoid ξ C

    ------------------------------------------------------------------------
    -- Multi-sorted algebras
    --------------------------------------------------------------------------
    -- A multi-sorted algebra is an indexed container.
    --
    -- * Sorts are indexes.
    --
    -- * Operators are commands/shapes.
    --
    -- * Arities/argument are responses/positions.
    --
    -- Closed terms (initial model) are given by the W type for a container,
    -- renamed to μ here (for least fixed-point).

    -- We assume a fixed signature (Sort, Ops).

    module _ (Sort : Set ℓˢ) (Ops : Container Sort Sort ℓᵒ ℓᵃ) where
      open Container Ops renaming
        ( Command   to  Op
        ; Response  to  Arity
        ; next      to  sort
        )

    -- We let letter $s$ range over sorts and $\mathit{op}$ over operators.

      variable
        s s'    : Sort
        op op'  : Op s

    ------------------------------------------------------------------------
    -- Models

      -- A model is given by an interpretation (Den $s$) for each sort $s$
      -- plus an interpretation (den $o$) for each operator $o$.

      record SetModel ℓᵐ : Set (ℓˢ ⊔ ℓᵒ ⊔ ℓᵃ ⊔ suc ℓᵐ) where
        field
          Den : Sort → Set ℓᵐ
          den : {s : Sort} → ⟦ Ops ⟧ Den s → Den s

      -- The setoid model requires operators to respect equality.
      -- The Func record packs a function (apply) with a proof (cong)
      -- that the function maps equals to equals.

      record SetoidModel ℓᵐ ℓᵉ : Set (ℓˢ ⊔ ℓᵒ ⊔ ℓᵃ ⊔ suc (ℓᵐ ⊔ ℓᵉ)) where
        field
          Den  :  Sort → Setoid ℓᵐ ℓᵉ
          den  :  {s : Sort} → Func (⟦ Ops ⟧s Den s) (Den s)

    ------------------------------------------------------------------------
    -- Terms

      -- To obtain terms with free variables, we add additional nullary
      -- operators, each representing a variable.
      --
      -- These are covered in the standard library FreeMonad module,
      -- albeit with the restriction that the operator and variable sets
      -- have the same size.

      Cxt = Sort → Set ℓᵒ

      variable
        Γ Δ : Cxt

      -- Terms with free variables in Var.

      module _ (Var : Cxt) where

        -- We keep the same sorts, but add a nullary operator for each variable.

        Ops⁺ : Container Sort Sort ℓᵒ ℓᵃ
        Ops⁺ = Ops ⋆C Var

        -- Terms with variables are then given by the W-type for the extended container.

        Tm = W Ops⁺

        -- We define nice constructors for variables and operator application
        -- via pattern synonyms.
        -- Note that the $f$ in constructor var' is a function from the empty set,
        -- so it should be uniquely determined.  However, Agda's equality is
        -- more intensional and will not identify all functions from the empty set.
        -- Since we do not make use of the axiom of function extensionality,
        -- we sometimes have to consult the extensional equality of the
        -- function setoid.

        pattern _∙_ op args  = sup (inj₂ op , args)
        pattern var' x f     = sup (inj₁ x , f    )
        pattern var x        = var' x _

      -- Letter $t$ ranges over terms, and $\mathit{ts}$ over argument vectors.

      variable
        t t' t₁ t₂ t₃  :  Tm Γ s
        ts ts'         :  (i : Arity op) → Tm Γ (sort _ i)

    ------------------------------------------------------------------------
    -- Parallel substitutions

      -- A substitution from Δ to Γ holds a term in Γ for each variable in Δ.

      Sub : (Γ Δ : Cxt) → Set _
      Sub Γ Δ = ∀{s} (x : Δ s) → Tm Γ s

      -- Application of a substitution.

      _[_] : (t : Tm Δ s) (σ : Sub Γ Δ) → Tm Γ s
      (var x  )  [ σ ] = σ x
      (op ∙ ts)  [ σ ] = op ∙ λ i → ts i [ σ ]

      -- Letter $σ$ ranges over substitutions.

      variable
        σ σ' : Sub Γ Δ

    ------------------------------------------------------------------------
    -- Interpretation of terms in a model
    ------------------------------------------------------------------------

      -- Given an algebra $M$ of set-size $ℓ^m$ and equality-size $ℓ^e$,
      -- we define the interpretation of an $s$-sorted term $t$ as element
      -- of $M(s)$ according to an environment $ρ$ that maps each variable
      -- of sort $s'$ to an element of $M(s')$.

      module _ {M : SetoidModel ℓᵐ ℓᵉ} where
        open SetoidModel M

        -- Equality in $M$'s interpretation of sort $s$.

        _≃_ : Den s .Carrier → Den s .Carrier → Set _
        _≃_ {s = s} = Den s ._≈_

        -- An environment for Γ maps each variable $x : Γ(s)$ to an element of $M(s)$.
        -- Equality of environments is defined pointwise.

        Env : Cxt → Setoid _ _
        Env Γ .Carrier   = {s : Sort} (x : Γ s) → Den s .Carrier
        Env Γ ._≈_ ρ ρ'  = {s : Sort} (x : Γ s) → ρ x ≃ ρ' x
        Env Γ .isEquivalence .IsEquivalence.refl   {s = s}   x = Den s .Setoid.refl
        Env Γ .isEquivalence .IsEquivalence.sym       h {s}  x = Den s .Setoid.sym   (h x)
        Env Γ .isEquivalence .IsEquivalence.trans  g  h {s}  x = Den s .Setoid.trans (g x) (h x)

        -- Interpretation of terms is iteration on the W-type.
        -- The standard library offers `iter' (on sets), but we need this to be a Func (on setoids).

        ⦅_⦆ : ∀{s} (t : Tm Γ s) → Func (Env Γ) (Den s)
        ⦅ var x      ⦆ .apply  ρ     = ρ x
        ⦅ var x      ⦆ .cong   ρ=ρ'  = ρ=ρ' x
        ⦅ op ∙ args  ⦆ .apply  ρ     = den .apply  (op    , λ i → ⦅ args i ⦆ .apply ρ)
        ⦅ op ∙ args  ⦆ .cong   ρ=ρ'  = den .cong   (refl  , λ i → ⦅ args i ⦆ .cong ρ=ρ')

        -- An equality between two terms holds in a model
        -- if the two terms are equal under all valuations of their free variables.

        Equal : ∀ {Γ s} (t t' : Tm Γ s) → Set _
        Equal {Γ} {s} t t' = ∀ (ρ : Env Γ .Carrier) → ⦅ t ⦆ .apply ρ ≃ ⦅ t' ⦆ .apply ρ

        -- This notion is an equivalence relation.

        isEquiv : IsEquivalence (Equal {Γ = Γ} {s = s})
        isEquiv {s = s} .IsEquivalence.refl  ρ       = Den s .Setoid.refl
        isEquiv {s = s} .IsEquivalence.sym   e ρ     = Den s .Setoid.sym (e ρ)
        isEquiv {s = s} .IsEquivalence.trans e e' ρ  = Den s .Setoid.trans (e ρ) (e' ρ)

    ------------------------------------------------------------------------
    -- Substitution lemma

        -- Evaluation of a substitution gives an environment.

        ⦅_⦆s : Sub Γ Δ → Env Γ .Carrier → Env Δ .Carrier
        ⦅ σ ⦆s ρ x = ⦅ σ x ⦆ .apply ρ

        -- Substitution lemma: ⦅t[σ]⦆ρ ≃ ⦅t⦆⦅σ⦆ρ

        substitution : (t : Tm Δ s) (σ : Sub Γ Δ) (ρ : Env Γ .Carrier) →
          ⦅ t [ σ ] ⦆ .apply ρ ≃ ⦅ t ⦆ .apply (⦅ σ ⦆s ρ)
        substitution (var x)    σ ρ = Den _ .Setoid.refl
        substitution (op ∙ ts)  σ ρ = den .cong (refl , λ i → substitution (ts i) σ ρ)

    ------------------------------------------------------------------------
    -- Equations

      -- An equation is a pair $t ≐ t'$ of terms of the same sort in the same context.

      record Eq : Set (ℓˢ ⊔ suc ℓᵒ ⊔ ℓᵃ) where
        constructor _≐_
        field
          {cxt}  : Sort → Set ℓᵒ
          {srt}  : Sort
          lhs    : Tm cxt srt
          rhs    : Tm cxt srt

      -- Equation $t ≐ t'$ holding in model $M$.

      _⊧_ : (M : SetoidModel ℓᵐ ℓᵉ) (eq : Eq) → Set _
      M ⊧ (t ≐ t') = Equal {M = M} t t'

      -- Sets of equations are presented as collection E : I → Eq
      -- for some index set I : Set ℓⁱ.

      -- An entailment/consequence $E ⊃ t ≐ t'$ is valid
      -- if $t ≐ t'$ holds in all models that satify equations $E$.

      module _ {ℓᵐ ℓᵉ} where

        _⊃_ : (E : I → Eq) (eq : Eq) → Set _
        E ⊃ eq = ∀ (M : SetoidModel ℓᵐ ℓᵉ) → (∀ i → M ⊧ E i) → M ⊧ eq

      -- Derivations
      --------------

      -- Equalitional logic allows us to prove entailments via the
      -- inference rules for the judgment $E ⊢ Γ ▹ t ≡ t'$.
      -- This could be coined as equational theory over a given
      -- set of equations $E$.
      -- Relation $E ⊢ Γ ▹ \_ ≡ \_$ is the least congruence over the equations $E$.

      data _⊢_▹_≡_ {I : Set ℓⁱ}
        (E : I → Eq) : (Γ : Cxt) (t t' : Tm Γ s) → Set (ℓˢ ⊔ suc ℓᵒ ⊔ ℓᵃ ⊔ ℓⁱ) where

        hyp    :  ∀ i → let t ≐ t' = E i in
                  E ⊢ _ ▹ t ≡ t'

        base   :  ∀ (x : Γ s) {f f' : (i : ⊥) → Tm _ (⊥-elim i)} →
                  E ⊢ Γ ▹ var' x f ≡ var' x f'

        app    :  (∀ i → E ⊢ Γ ▹ ts i ≡ ts' i) →
                  E ⊢ Γ ▹ (op ∙ ts) ≡ (op ∙ ts')

        sub    :  E ⊢ Δ ▹ t ≡ t' →
                  ∀ (σ : Sub Γ Δ) →
                  E ⊢ Γ ▹ (t [ σ ]) ≡ (t' [ σ ])

        refl   :  ∀ (t : Tm Γ s) →
                  E ⊢ Γ ▹ t ≡ t

        sym    :  E ⊢ Γ ▹ t ≡ t' →
                  E ⊢ Γ ▹ t' ≡ t

        trans  :  E ⊢ Γ ▹ t₁ ≡ t₂ →
                  E ⊢ Γ ▹ t₂ ≡ t₃ →
                  E ⊢ Γ ▹ t₁ ≡ t₃

    ------------------------------------------------------------------------
    -- Soundness of the inference rules

      -- We assume a model $M$ that validates all equations in $E$.

      module Soundness {I : Set ℓⁱ} (E : I → Eq) (M : SetoidModel ℓᵐ ℓᵉ)
        (V : ∀ i → M ⊧ E i) where
        open SetoidModel M

        -- In any model $M$ that satisfies the equations $E$,
        -- derived equality is actual equality.

        sound : E ⊢ Γ ▹ t ≡ t' → M ⊧ (t ≐ t')

        sound (hyp i)                        =  V i
        sound (app {op = op} es) ρ           =  den .cong (refl , λ i → sound (es i) ρ)
        sound (sub {t = t} {t' = t'} e σ) ρ  =  begin
          ⦅ t [ σ ]   ⦆ .apply ρ   ≈⟨ substitution {M = M} t σ ρ ⟩
          ⦅ t         ⦆ .apply ρ'  ≈⟨ sound e ρ' ⟩
          ⦅ t'        ⦆ .apply ρ'  ≈⟨ substitution {M = M} t' σ ρ ⟨
          ⦅ t' [ σ ]  ⦆ .apply ρ   ∎
          where
          open SetoidReasoning (Den _)
          ρ' = ⦅ σ ⦆s ρ

        sound (base x {f} {f'})              =  isEquiv {M = M} .IsEquivalence.refl {var' x λ()}

        sound (refl t)                       =  isEquiv {M = M} .IsEquivalence.refl {t}
        sound (sym {t = t} {t' = t'} e)      =  isEquiv {M = M} .IsEquivalence.sym
                                                {x = t} {y = t'} (sound e)
        sound (trans  {t₁ = t₁} {t₂ = t₂}
                      {t₃ = t₃} e e')        =  isEquiv {M = M} .IsEquivalence.trans
                                                {i = t₁} {j = t₂} {k = t₃} (sound e) (sound e')

    ------------------------------------------------------------------------
    -- Birkhoff's completeness theorem
    ------------------------------------------------------------------------

      -- Birkhoff proved that any equation $t ≐ t'$ is derivable from $E$
      -- when it is valid in all models satisfying $E$.  His proof (for
      -- single-sorted algebras) is a blue print for many more
      -- completeness proofs.  They all proceed by constructing a
      -- universal model aka term model.  In our case, it is terms
      -- quotiented by derivable equality $E ⊢ Γ ▹ \_ ≡ \_$.  It then
      -- suffices to prove that this model satisfies all equations in $E$.

    ------------------------------------------------------------------------
    -- Universal model

      -- A term model for $E$ and $Γ$ interprets sort $s$ by (Tm Γ s) quotiented by $E ⊢ Γ ▹ \_ ≡ \_$.

      module TermModel {I : Set ℓⁱ} (E : I → Eq) where
        open SetoidModel

        -- Tm Γ s quotiented by E⊢Γ▹·≡·.

        TmSetoid : Cxt → Sort → Setoid _ _
        TmSetoid Γ s .Carrier                             = Tm Γ s
        TmSetoid Γ s ._≈_                                 = E ⊢ Γ ▹_≡_
        TmSetoid Γ s .isEquivalence .IsEquivalence.refl   = refl _
        TmSetoid Γ s .isEquivalence .IsEquivalence.sym    = sym
        TmSetoid Γ s .isEquivalence .IsEquivalence.trans  = trans

        -- The interpretation of an operator is simply the operator.
        -- This works because $E⊢Γ▹\_≡\_$ is a congruence.

        tmInterp : ∀ {Γ s} → Func (⟦ Ops ⟧s (TmSetoid Γ) s) (TmSetoid Γ s)
        tmInterp .apply (op , ts) = op ∙ ts
        tmInterp .cong (refl , h) = app h

        -- The term model per context Γ.

        M : Cxt → SetoidModel _ _
        M Γ .Den = TmSetoid Γ
        M Γ .den = tmInterp

        -- The identity substitution σ₀ maps variables to themselves.

        σ₀ : {Γ : Cxt} → Sub Γ Γ
        σ₀ x = var' x  λ()

        -- σ₀ acts indeed as identity.

        identity : (t : Tm Γ s) → E ⊢ Γ ▹ t [ σ₀ ] ≡ t
        identity (var x)    = base x
        identity (op ∙ ts)  = app λ i → identity (ts i)

        -- Evaluation in the term model is substitution $E ⊢ Γ ▹ ⦅t⦆σ ≡ t[σ]$.
        -- This would even hold "up to the nose" if we had function extensionality.

        evaluation : (t : Tm Δ s) (σ : Sub Γ Δ) → E ⊢ Γ ▹ (⦅_⦆ {M = M Γ} t .apply σ) ≡ (t [ σ ])
        evaluation (var x)    σ = refl (σ x)
        evaluation (op ∙ ts)  σ = app (λ i → evaluation (ts i) σ)

        -- The term model satisfies all the equations it started out with.

        satisfies : ∀ i → M Γ ⊧ E i
        satisfies i σ = begin
          ⦅ tₗ ⦆ .apply σ  ≈⟨ evaluation tₗ σ ⟩
          tₗ [ σ ]         ≈⟨ sub (hyp i) σ ⟩
          tᵣ [ σ ]         ≈⟨ evaluation tᵣ σ ⟨
          ⦅ tᵣ ⦆ .apply σ  ∎
          where
          open SetoidReasoning (TmSetoid _ _)
          tₗ  = E i .Eq.lhs
          tᵣ = E i .Eq.rhs

    ------------------------------------------------------------------------
    -- Completeness

    -- Birkhoff's completeness theorem \citeyearpar{birkhoff:1935}:
    -- Any valid consequence is derivable in the equational theory.

      module Completeness {I : Set ℓⁱ} (E : I → Eq) {Γ s} {t t' : Tm Γ s} where
        open TermModel E

        completeness : E ⊃ (t ≐ t') → E ⊢ Γ ▹ t ≡ t'
        completeness V =     begin
          t                  ≈˘⟨ identity t ⟩
          t  [ σ₀ ]          ≈˘⟨ evaluation t σ₀ ⟩
          ⦅ t   ⦆ .apply σ₀  ≈⟨ V (M Γ) satisfies σ₀ ⟩
          ⦅ t'  ⦆ .apply σ₀  ≈⟨ evaluation t' σ₀ ⟩
          t' [ σ₀ ]          ≈⟨ identity t' ⟩
          t'                 ∎
          where open SetoidReasoning (TmSetoid Γ s)