Setoid.Signatures

The signature-to-setoid functor

This is the Setoid.Signatures module of the Agda Universal Algebra Library.

It collects the two signature-generic constructions that translate an ordinary signature into a signature over a setoid domain: the polynomial-functor lifting ⟨_⟩ and its companion EqArgs. Each takes the signature as its own argument — explicitly for ⟨_⟩, as an implicit {𝑆} for EqArgs — and reads no ambient signature, so they live in a module with no {𝑆 : Signature 𝓞 𝓥} parameter. It is the setoid-level companion to Overture.Signatures.

Keeping them here — rather than inside the signature-parameterized Setoid.Algebras.Basic — matters for more than tidiness. In a module parameterized by {𝑆 : Signature 𝓞 𝓥}, every definition gets that module parameter silently prepended, whether or not it uses it. For Algebra, _^_, 𝔻[_], … that is harmless: their types mention the module's 𝑆, so it is recovered from context at each use site. But ⟨_⟩ and EqArgs take their own signature argument and never refer to the module's parameter, so the prepended {𝑆} is left unconstrained — a hand-written use site stalls on it as an unsolvable metavariable. Defining them in this non-parameterized module removes the spurious parameter at the source. Setoid.Algebras.Basic re-exports both names, so importing them from there is unaffected.

The setoid-algebra approach was inspired by Andreas Abel's formalization of Birkhoff's completeness theorem; see: http://www.cse.chalmers.se/~abela/agda/MultiSortedAlgebra.pdf.

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

module Setoid.Signatures where

-- Imports from the Agda and the Agda Standard Library --------------------
open import Agda.Primitive   using () renaming ( Set to Type )
open import Data.Product     using ( _,_ ; Σ-syntax )
open import Level            using ( Level ; _⊔_ )
open import Relation.Binary  using ( Setoid ; IsEquivalence )

open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)

-- Imports from the Agda Universal Algebra Library ----------------------
open import Overture  using ( 𝓞 ; 𝓥 ; Signature ; OperationSymbolsOf ; ArityOf )

private variable α ρ : Level

open Setoid
 using ( _≈_ ; Carrier )
 renaming ( refl to reflS ; sym to symS ; trans to transS ; isEquivalence to isEqv )

EqArgs is the equality on the argument tuples of a pair of operation symbols. Given a proof f ≡ g that the two symbols agree, two tuples are EqArgs-related when they are pointwise equal in the underlying setoid A.

EqArgs : {𝑆 : Signature 𝓞 𝓥} (A : Setoid α ρ)
  → ∀{f g} → f ≡ g → (ArityOf 𝑆 f → Carrier A) → (ArityOf 𝑆 g → Carrier A)
  → Type (𝓥 ⊔ ρ)

EqArgs A ≡.refl u v = ∀ i → u i ≈ᴬ v i
  where open Setoid A using () renaming ( _≈_ to _≈ᴬ_ )

⟨ 𝑆 ⟩ A is the setoid whose carrier is a single operation symbol paired with a tuple of its arguments drawn from A, and whose equality is EqArgs. This is the polynomial functor of the signature 𝑆, lifted to setoids.

open IsEquivalence using( refl ; sym ; trans )

⟨_⟩ : Signature 𝓞 𝓥 → Setoid α ρ → Setoid (𝓞 ⊔ 𝓥 ⊔ α) (𝓞 ⊔ 𝓥 ⊔ ρ)
⟨ 𝑆 ⟩ A .Carrier = Σ[ f ∈ OperationSymbolsOf 𝑆 ] (ArityOf 𝑆 f → A .Carrier)
⟨ 𝑆 ⟩ A ._≈_ (f , u) (g , v) = Σ[ eqv ∈ f ≡ g ] EqArgs A eqv u v
⟨ 𝑆 ⟩ A .isEqv .refl = ≡.refl , λ _ → reflS A
⟨ 𝑆 ⟩ A .isEqv .sym (≡.refl , g) = ≡.refl , λ i → symS A (g i)
⟨ 𝑆 ⟩ A .isEqv .trans (≡.refl , g) (≡.refl , h) = ≡.refl , λ i → transS  A (g i) (h i)