Setoid.Varieties.FreeSubstitution

A substitution kit for derivable equality

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

Substitution _[_] (Setoid.Terms.Basic) pushes into a node pointwise,

(node f ts) [ σ ] = node f (λ i → ts i [ σ ]).

When ts is a finite tuple written as a pattern-matching lambda, say, λ { 0F → s ; 1F → t }, the natural way to write a binary term is, e.g., s · t = node ∙-Op (λ { 0F → s ; 1F → t }).

Unfortunately, the result node f (λ i → ts i [ σ ]) is not definitionally equal to a freshly rebuilt term

s [ σ ] · t [ σ ] = node ∙-Op (λ { 0F → s [ σ ] ; 1F → t [ σ ] }),

since a pattern-matching lambda does not reduce under a variable index i, and bridging the two position functions needs function extensionality, which is unavailable under --safe / --cubical-compatible.¹

The practical bite is that the obvious way to instantiate an equation at compound terms fails: sub (hyp i) σ produces a goal in _[ σ ]-form that will not match a readable, rebuilt term, so a multi-step rewrite like a four-fold reassociation cannot be written directly.

The fix is small, because the bookkeeping half of the kit is already proved: the _≐_-level laws []-unitˡ (left unit, the issue's []-ℊ), []-unitʳ, []-assoc, and []-cong live in Setoid.Terms.Monad. What is added here is the bridge between the two equalities on terms — the inductive equality _≐_ of Setoid.Terms.Basic and the derivable equality _⊢_▹_≈_ of Setoid.Varieties.SoundAndComplete:

• ≐→⊢ — every _≐_-equality is derivable. Two terms that are _≐_ (same shape, equal variables at the leaves) are equal in every equational theory, by refl at the leaves and the congruence rule app at the nodes. This is exactly the tool for rewriting a _[ σ ]-form into the rebuilt term it agrees with pointwise: the rebuild is a _≐_-fact (a finite, mechanical gnl / ≐-isRefl match), and ≐→⊢ turns it into a derivation step.
• sub▹ — instantiate a derivation at a substitution and land on readable end terms. It packages sub between two ≐→⊢ bridges, so a consumer writes sub▹ d σ l≐pσ qσ≐r and gets E ⊢ Γ ▹ l ≈ r directly.

The worked four-fold reassociation that motivated the substitution kit is in Examples.Setoid.FreeSemigroup, built from one application of sub▹ (a generic assoc▹ that instantiates associativity at arbitrary subterms) plus the congruence rule.

The kit also has a semantic face, used by the converse Maltsev conditions:

• subhom / renhom — a substitution acts on the relatively free algebra 𝔽[_] (Setoid.Varieties.SoundAndComplete) as a homomorphism, whose congruence is precisely the sub rule;
• cg-pair→⊢ / cg-pairs→⊢ — the free-algebra congruence/derivability bridge: a membership in a principal congruence Cg ❴ a , b ❵ of 𝔽[ Δ ] — or in the join of two principal congruences — becomes a derivable equation after any substitution that collapses the generating pair(s).

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

open import Overture using ( 𝓞 ; 𝓥 ; Signature )

module Setoid.Varieties.FreeSubstitution {𝑆 : Signature 𝓞 𝓥} where

-- Imports from Agda and the Agda Standard Library ----------------------------
open import Agda.Primitive   using () renaming ( Set to Type )
open import Data.Product     using ( _,_ ; proj₁ )
open import Data.Sum.Base    using ( inj₁ ; inj₂ )
open import Function         using ( Func )
open import Level            using ( Level )
open import Relation.Binary  using () renaming ( _⇒_ to _⊆_ )

import Relation.Binary.PropositionalEquality as ≡

-- Imports from the Agda Universal Algebra Library ----------------------------
open import Overture.Terms                      {𝑆 = 𝑆} using ( Term ; ℊ )
open import Setoid.Algebras.Basic               {𝑆 = 𝑆} using ( 𝔻[_] )
open import Setoid.Congruences.Generation       {𝑆 = 𝑆} using ( Gen ; Cg ; base
                                                               ; symmetric ; _∨_ ; _∪ᵣ_
                                                               ; module principal )
open import Setoid.Homomorphisms.Basic                   using ( hom ; mkIsHom )
open import Setoid.Homomorphisms.Kernels                 using ( kercon )
open import Setoid.Homomorphisms.Properties              using ( Cg⊆ker )
open import Setoid.Terms.Basic                  {𝑆 = 𝑆} using ( _≐_ ; Sub ; _[_] )
open import Setoid.Varieties.SoundAndComplete   {𝑆 = 𝑆} using ( Eq ; _⊢_▹_≈_
                                                               ; module FreeAlgebra )

open _≐_         using ( rfl ; gnl )
open _⊢_▹_≈_     using ( app ; sub ; refl ; trans )

private variable
  χ ι : Level
  Γ Δ : Type χ
  I   : Type ι

Derivable equality refines term equality

Every _≐_-equality is derivable in any theory E. The leaf case is the reflexivity rule (the variables are equal, so the terms are literally equal); the node case is the congruence rule app applied to the inductive hypotheses at the positions. No clause inspects the equation set E, so this holds uniformly.

≐→⊢ : {E : I → Eq} {s t : Term Γ} → s ≐ t → E ⊢ Γ ▹ s ≈ t
≐→⊢ (rfl ≡.refl)  = refl
≐→⊢ (gnl ps)      = app (λ i → ≐→⊢ (ps i))

Instantiating a derivation at compound terms

sub▹ d σ substitutes σ into a derivation d : E ⊢ Δ ▹ p ≈ q and rewrites both ends to readable terms supplied by the caller: given l ≐ p [ σ ] and q [ σ ] ≐ r, it returns E ⊢ Γ ▹ l ≈ r. This is the clean way to use an equation at compound terms — the _≐_ arguments are the mechanical "rebuild" bridges, and sub▹ hides the _[ σ ]-form behind them.

sub▹ : {E : I → Eq} {p q : Term Δ} (d : E ⊢ Δ ▹ p ≈ q) (σ : Sub Γ Δ)
       {l r : Term Γ} → l ≐ p [ σ ] → q [ σ ] ≐ r → E ⊢ Γ ▹ l ≈ r
sub▹ d σ l≐pσ qσ≐r = trans (≐→⊢ l≐pσ) (trans (sub d σ) (≐→⊢ qσ≐r))

The substitution-induced homomorphism

Fix a theory E : I → Eq. A substitution σ : Sub Γ Δ (each Δ-variable to a Γ-term) induces the homomorphism subhom σ : 𝔽[ Δ ] → 𝔽[ Γ ] on the relatively free algebra whose underlying map is _[ σ ]. It respects derivable equality by the sub rule, and the homomorphism square holds by refl because (node f ts) [ σ ] is node f (λ i → ts i [ σ ]) on the nose.

module _ {Γ Δ : Type χ} {I : Type ι} (E : I → Eq) where
  open FreeAlgebra E using ( 𝔽[_] )

  subhom : (σ : Sub Γ Δ) → hom 𝔽[ Δ ] 𝔽[ Γ ]
  subhom σ = subfunc , mkIsHom (λ {f}{a} → refl)
    where
    subfunc : Func 𝔻[ 𝔽[ Δ ] ] 𝔻[ 𝔽[ Γ ] ]
    subfunc = record { to = _[ σ ] ; cong = λ {p}{q} pq → sub pq σ }

The special case of a plain variable renaming r : Δ → Γ is subhom (ℊ ∘ r).

  renhom : (r : Δ → Γ) → hom 𝔽[ Δ ] 𝔽[ Γ ]
  renhom r = subhom (λ v → ℊ (r v))

The principal-pair bridge

Combining the substitution homomorphism with Cg⊆ker (Setoid.Homomorphisms.Properties) yields the free-algebra congruence/derivability bridge: given a substitution σ that collapses the pair (a , b) — i.e. E ⊢ Γ ▹ a [ σ ] ≈ b [ σ ] is derivable — every pair (s , t) in the principal congruence Cg ❴ a , b ❵ of 𝔽[ Δ ] becomes derivably equal after σ. This is how the converse Maltsev conditions read term identities off congruences of the free algebra (Setoid.Varieties.Maltsev.Permutability, Setoid.Varieties.Maltsev.Distributivity).

  open principal 𝔽[ Δ ]

  cg-pair→⊢ : (σ : Sub Γ Δ)(a b : Term Δ)
    → E ⊢ Γ ▹ a [ σ ] ≈ b [ σ ]
    → {s t : Term Δ} → Gen ❴ a , b ❵ s t → E ⊢ Γ ▹ s [ σ ] ≈ t [ σ ]
  cg-pair→⊢ σ a b coll = Cg⊆ker (subhom σ) incl
    where
    incl : ❴ a , b ❵ ⊆ proj₁ (kercon (subhom σ))
    incl pᵣ = coll

The converse of Day's theorem (Setoid.Varieties.Maltsev.Modularity) needs the same bridge for the join of two principal congruences: two of the congruences in Day's construction collapse two generator pairs at once, so their collapsing substitutions must kill both. Given a substitution σ that collapses the pair (a , b) and the pair (c , d), every pair in Cg ❴ a , b ❵ ∨ Cg ❴ c , d ❵ becomes derivably equal after σ. The proof is the same Cg⊆ker instance: the union of the two generating congruences is included in the kernel componentwise, each component by cg-pair→⊢.

  cg-pairs→⊢ : (σ : Sub Γ Δ)(a b c d : Term Δ)
    → E ⊢ Γ ▹ a [ σ ] ≈ b [ σ ]
    → E ⊢ Γ ▹ c [ σ ] ≈ d [ σ ]
    → {s t : Term Δ} → proj₁ (Cg ❴ a , b ❵ ∨ Cg ❴ c , d ❵) s t
    → E ⊢ Γ ▹ s [ σ ] ≈ t [ σ ]
  cg-pairs→⊢ σ a b c d coll-ab coll-cd = Cg⊆ker (subhom σ) incl
    where
    incl : (Cg ❴ a , b ❵ ∪ᵣ Cg ❴ c , d ❵) ⊆ proj₁ (kercon (subhom σ))
    incl (inj₁ p) = cg-pair→⊢ σ a b coll-ab p
    incl (inj₂ q) = cg-pair→⊢ σ c d coll-cd q

Smoke test: recovering a derivable identity from a principal congruence

A small end-to-end consumer. Fix two variables u, v, a substitution σ that merges them (σ u, σ v are derivably equal), and the principal congruence Cg ❴ ℊ u , ℊ v ❵. Then every pair in that congruence is recovered as a derivable equation after σ; in particular the generators themselves, and (by symmetry) the swapped pair.

module _
  {Γ : Type χ}
  {I : Type ι}
  (E : I → Eq)
  (σ : Sub Γ Γ)  (u v : Γ)
  (merge : E ⊢ Γ ▹ σ u ≈ σ v)
  where
  open FreeAlgebra E using ( 𝔽[_] )
  open principal 𝔽[ Γ ]

  recover : {s t : Term Γ} → Gen ❴ ℊ u , ℊ v ❵ s t → E ⊢ Γ ▹ s [ σ ] ≈ t [ σ ]
  recover = cg-pair→⊢ E σ (ℊ u) (ℊ v) merge

  recover-gen : E ⊢ Γ ▹ σ u ≈ σ v
  recover-gen = recover (base pᵣ)

  recover-swap : E ⊢ Γ ▹ σ v ≈ σ u
  recover-swap = recover (symmetric (base pᵣ))

---

---

1. This is the same Fin n η-gap that the M4-5 development meets repeatedly; see ADR-002 §6. ↩