---
layout: default
file: "src/Setoid/Varieties/Invariance.lagda.md"
title: "Setoid.Varieties.Invariance module"
date: "2026-06-12"
author: "the agda-algebras development team"
---

### 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.

```text
                  Ο† ✢_
        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`][Setoid.Algebras.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`][Setoid.Algebras.Reduct] is itself a
`Setoid/` construction (both relocated from `Classical/` by
[ADR-006](../../docs/adr/006-signature-morphism-category.md), M4-16).  It opens the
two-signature `Setoid/Varieties/` area that M4-5g (reduct classes of varieties) extends.

<!--
```agda
{-# 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.

```agda
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.

```agda
  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.

```agda
  ⊧-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."