Skip to content

Setoid.Varieties.Invariance

Reduct-invariance of satisfaction

This is the Setoid.Varieties.Invariance module of the Agda Universal Algebra Library.

This module proves the reduct-invariance of satisfaction, which is the primary pay-off of expressing the reduct as a functor.

For a signature morphism Ο† : 𝑆₁ β†’ 𝑆₂, an 𝑆₂-algebra 𝑨, and 𝑆₁-terms s , t, we have

reduct Ο† 𝑨 ⊧ s β‰ˆ t   if and only if   𝑨 ⊧ Ο† ✢ s β‰ˆ Ο† ✢ t.

In words: to check an equation against the poorer view of 𝑨 (the reduct, which sees only the 𝑆₁-operations) is the same as checking the translated equation against 𝑨 itself.

Model theorists know this as (the equational case of) the satisfaction condition of institutions,1 and universal algebraists use it tacitly every time we say "a monoid satisfies the semigroup laws."

Why this is naturality of the fold

Nothing about the theorem is specific to satisfaction; the satisfaction statement is the shadow of one commuting triangle of interpretation maps. Fix an environment Ξ· : X β†’ π•Œ[ 𝑨 ] (note 𝑨 and reduct Ο† 𝑨 have the same carrier, so one environment serves both, and Ο† ✢_ fixes variables, so no translation of Ξ· is needed).

Evaluation of 𝑆₁-terms in the reduct, and of 𝑆₂-terms in 𝑨, fit around the term translation.

                  Ο† ✢_
        Term₁ X ────────→ Termβ‚‚ X

             β•²             β”‚  ⟦_⟧ in 𝑨
    ⟦_⟧ in     β•²           β”‚  (the 𝑆₂-fold)
    reduct Ο† 𝑨   β•²         β”‚
                   β•²       |
                    β•²      |
                     β•²     |
                      β†˜    ↓

                      π•Œ[ 𝑨 ]

reduct-interp below proves this triangle commutes, by structural induction on the term. Both routes are folds β€” unique homomorphic extensions out of term algebras β€” and the triangle is precisely the naturality of the fold with respect to the natural transformation ⟦ Ο† ⟧ : ⟨ 𝑆₁ ⟩ ⟹ ⟨ 𝑆₂ ⟩ induced by Ο† (M4-5b, Setoid.Signatures.Functor): unwinding the node case of the proof, the inductive step is exactly "precompose with ⟦ Ο† ⟧'s component, then interpret" β€” which is the defining clause of reduct. Once the triangle commutes, both invariance directions are two-line equational rearrangements: an equation ⟦s⟧ β‰ˆ ⟦t⟧ holds on one side of the triangle iff it holds on the other.

The companion naturality in the algebra argument β€” fix the signature, vary the algebra along a homomorphism β€” is free-lift-natural / comm-hom-term (Setoid.Terms.Properties, Setoid.Terms.Operations). The two naturalities together say the interpretation pairing (𝑨 , t) ↦ ⟦ t ⟧ᴬ is functorial in both coordinates, which is the full content of "⟦_⟧ is the unique fold."

What this absorbs, and the M3-5 measurement

M3-6 discharged theory obligations for reduct-derived forgetfuls by hand: the Th-Semigroup obligation inside monoidβ†’semigroup (Classical.Structures.Monoid) pivots through curried associativity using per-signature interp-node bridges, each paying the Fin n Ξ·-gap (ADR-002 Β§1, the M3-5 finding) once. ⊧-reduct replaces that pattern: the general lemma is proved once, by structural induction over abstract positions, and β€” this is the measurement the issue asks to record β€” the M3-5 binary-node-bridge obstruction does not appear at the functorial level. No clause here matches refl against a neutral ArityOf 𝑆 f ≑ Fin 2, no interp-node family is needed, and no Fin Ξ·-bridge is paid: the induction never compares a concrete Fin-pattern lambda against an abstract tuple. What residue remains is per-theory, not per-signature: a concrete theory written with pair-style Fin-lambdas must be aligned with its translation up to the term equality _≐_ (a finite, mechanical pattern-match; see the demonstration in Classical.Categories.Forgetful) β€” and that alignment is ≐-provable where a propositional ≑ would be funext-blocked. Conclusion: the obstruction dissolves functorially; only its benign, provable shadow survives, in the concrete theories themselves.

This module lives in Setoid.Varieties: reduct-invariance of satisfaction is general universal algebra, and its object map reduct is itself a Setoid/ construction (both relocated from Classical/ by ADR-006, M4-16). It opens the two-signature Setoid/Varieties/ area that M4-5g (reduct classes of varieties) extends.

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

module Setoid.Varieties.Invariance where

-- Imports from Agda and the Agda Standard Library ----------------------------
open import Agda.Primitive                 using () renaming ( Set to Type )
open import Data.Product                   using ( _,_ )
open import Function                       using ( Func )
open import Level                          using ( Level )
open import Relation.Binary                using ( Setoid )

open import Relation.Binary.PropositionalEquality using (refl) -- as ≑

-- Imports from the Agda Universal Algebra Library ----------------------------
open import Overture.Signatures            using ( π“ž ; π“₯ ; Signature )
open import Overture.Signatures.Morphisms  using ( SigMorphism ; ΞΊ )
open import Overture.Terms                 using ( Term ; β„Š ; node )
open import Overture.Terms.Translation     using ( _✢_ )
open import Setoid.Algebras.Basic          using ( Algebra ; 𝔻[_] ; π•Œ[_] )
open import Setoid.Algebras.Reduct         using ( reduct )

open import Setoid.Terms.Basic          using (module Environment) --        as TermsBasic
import Setoid.Varieties.EquationalLogic    as EqLogic

open Algebra using ( Interp )
open Func using ( cong ) renaming ( to to _⟨$⟩_ )

private variable
  Ξ± ρ Ο‡ : Level
  X : Type Ο‡

Naturality of the fold along a signature morphism

Everything below is parameterized by the morphism Ο† and the 𝑆₂-algebra 𝑨. The two Environment instances interpret 𝑆₁-terms in reduct Ο† 𝑨 and 𝑆₂-terms in 𝑨; the two _⊧_β‰ˆ_ instances are the corresponding satisfaction relations.

module _ {𝑆₁ 𝑆₂ : Signature π“ž π“₯} (Ο† : SigMorphism 𝑆₁ 𝑆₂) (𝑨 : Algebra {𝑆 = 𝑆₂} Ξ± ρ) where
  open Environment {𝑆 = 𝑆₁} (reduct Ο† 𝑨) using () renaming ( ⟦_⟧ to ⟦_βŸ§β‚ )
  open Environment {𝑆 = 𝑆₂} 𝑨 using () renaming ( ⟦_⟧ to ⟦_βŸ§β‚‚ )
  open Setoid 𝔻[ 𝑨 ] using ( _β‰ˆ_ ) renaming (refl to β‰ˆrefl; sym to β‰ˆsym ; trans to β‰ˆtrans )
  open EqLogic {𝑆 = 𝑆₁} using () renaming ( _⊧_β‰ˆ_ to _βŠ§β‚_β‰ˆ_ )
  open EqLogic {𝑆 = 𝑆₂} using () renaming ( _⊧_β‰ˆ_ to _βŠ§β‚‚_β‰ˆ_ )

The commuting triangle: interpreting an 𝑆₁-term in the reduct is interpreting its translation in 𝑨, under any environment. At a leaf both sides look up the variable. At a node, the reduct's interpretation is "apply the interpretation in 𝑨 of ΞΉ Ο† f to the ΞΊ Ο† f-reindexed arguments" β€” definitionally, by the defining clause of reduct β€” and the translation's node clause performs the same reindexing syntactically, so the two sides agree position by position, by the inductive hypothesis at the reindexed subterms. Note what does not happen: no arity is ever compared to a concrete Fin n, so the without-K unifier is never asked to invert anything.

  reduct-interp : (t : Term X) (Ξ· : X β†’ π•Œ[ 𝑨 ]) β†’ ⟦ t βŸ§β‚ ⟨$⟩ Ξ· β‰ˆ ⟦ Ο† ✢ t βŸ§β‚‚ ⟨$⟩ Ξ·
  reduct-interp (β„Š x) Ξ· = β‰ˆrefl
  reduct-interp (node f ts) Ξ· =
    cong (Interp 𝑨) (refl , Ξ» j β†’ reduct-interp (ts (ΞΊ Ο† f j)) Ξ·)

The satisfaction condition

Satisfaction is the interpretation triangle quantified over environments, so each direction of the invariance is a trans-sandwich of the triangle around the given satisfaction proof. Recall 𝑨 ⊧ p β‰ˆ q unfolds to "for every environment Ξ·, ⟦ p ⟧ Ξ· β‰ˆ ⟦ q ⟧ Ξ·"; environments transfer across the two sides on the nose because the carrier of the reduct is the carrier of 𝑨 and translation fixes variables.

⊧-reduct is the direction that discharges theory obligations of reduct-derived forgetful functors (a monoid's associativity, translated, is the semigroup associativity its reduct must satisfy); ⊧-expand is the converse, the direction used when transporting equational facts from a reduct up to its expansion.

  ⊧-reduct : {s t : Term X} β†’ 𝑨 βŠ§β‚‚ (Ο† ✢ s) β‰ˆ (Ο† ✢ t) β†’ reduct Ο† 𝑨 βŠ§β‚ s β‰ˆ t
  ⊧-reduct {s = s} {t} A⊧ η =
    β‰ˆtrans (reduct-interp s Ξ·) (β‰ˆtrans (A⊧ Ξ·) (β‰ˆsym (reduct-interp t Ξ·)))

  ⊧-expand : {s t : Term X} β†’ reduct Ο† 𝑨 βŠ§β‚ s β‰ˆ t β†’ 𝑨 βŠ§β‚‚ Ο† ✢ s β‰ˆ Ο† ✢ t
  ⊧-expand {s = s} {t} R⊧ η =
    β‰ˆtrans (β‰ˆsym (reduct-interp s Ξ·)) (β‰ˆtrans (R⊧ Ξ·) (reduct-interp t Ξ·))

Together the two directions are the biconditional promised at the top. They are deliberately kept as two one-directional lemmas rather than packaged into a single iff record: every consumer uses exactly one direction, and the unpacked forms compose directly with the satisfaction proofs the Classical theories carry.

  1. Goguen and Burstall's slogan is, "Truth is invariant under change of notation." ↩