---
layout: default
file: "src/Setoid/Congruences/Certificates/Congruence.lagda.md"
title: "Setoid.Congruences.Certificates.Congruence module (The Agda Universal Algebra Library)"
date: "2026-07-22"
author: "the agda-algebras development team"
---

### The per-congruence certificate checker (obligations C1–C3)

This is the [Setoid.Congruences.Certificates.Congruence][] module of the [Agda Universal Algebra Library][].

Fix a finite finitary algebra — an algebra `𝑨` with carrier-finiteness data
`𝑭` ([Setoid.Algebras.Finite][]) and signature-finiteness data `𝑺`
([Setoid.Signatures.Finite][]).  A per-congruence certificate
(`CgCert`{.AgdaRecord} of [Setoid.Congruences.Certificates.Schema][]) claims

> the partition presented by the parent vector  `≑  Cg (fromPairs P)`

for its seed list `P`.

This module is the checker for that claim.  The *claimed congruence* is the *table
relation* of the parent vector: two carrier elements are related when their
enumeration indices have the same parent — two constant-time lookups and one
`Fin`{.AgdaDatatype} equality, so the relation is decidable with no appeal to the
specification-grade decision procedure `Cg-dec`{.AgdaFunction},[^1]
which never appears here.

The checker obligations, each search-free and linear in the trace and table size,
are as follows:

+  **C1 (trace soundness)**.  Every merge of the Freese trace is derivable:
   seed entries point into `P`, and translate entries apply one
   `compatible`{.AgdaInductiveConstructor} rule of the generation datatype
   `Gen`{.AgdaDatatype} ([Setoid.Congruences.Generation][]) to an earlier merge.
   The checker *constructs* the `Gen`{.AgdaDatatype} derivations by a single
   fold over the trace — it never decides `Gen`{.AgdaDatatype}-membership.
+  **C2 (claimed ⊆ generated)**.  The obvious implementation, option (a), checks
   each forest edge of the claimed vector for membership in the trace's merged
   pairs.  Implementing against honest engine traces shows option (a) as literally
   stated is unattainable: the run's merged
   pairs need not contain the *normal-form* edges, because normal form re-roots
   every block at its least element after the run.  We therefore implement the
   alternative, option (b), in its simplest form: **replay** the trace's
   unions through an eager re-pointing root vector — no ranks, no path
   compression; those are engine-side devices — carrying a
   `Gen`{.AgdaDatatype}-proof invariant, and then align the replayed partition
   with the claimed vector by two linear sweeps (`Covers`{.AgdaFunction}).
   Cost: `O(n · |trace|)` root updates, one pass, no search.
+  **C3 (generated ⊆ claimed)**.  The claimed partition contains the seed pairs
   (`Respects`{.AgdaFunction}) and is a congruence: as a partition it is an
   equivalence for free, and operation-compatibility is checked on **one
   translate step per coordinate per tuple** (`EdgeCompat`{.AgdaFunction}) —
   the pair `(t , t [ c ]≔ parent (t c))` for every basic operation, coordinate,
   and argument tuple, which is Freese's `O(r · ‖A‖)` bound of unary polynomial
   translates times forest edges.  Compatibility for arbitrary pointwise-related
   tuples then follows by walking the coordinates and detouring through the
   roots, with no further checking.  `Cg-least`{.AgdaFunction} closes the
   inclusion.

The headline theorems `table≑Cg`{.AgdaFunction} (with a trace) and
`table≑CgEdges`{.AgdaFunction} (the trace-free special case where the seeds are
the vector's own forest edges, used for whole-lattice congruence lists) deliver
the claim as an honest `_≑_`{.AgdaFunction} at the working congruence level.

Every hypothesis is decidable, and each decider is a bounded sweep of
`Fin`{.AgdaDatatype} comparisons; the whole-lattice checker
([Setoid.Congruences.Certificates.Lattice][]) instantiates them wholesale.

<!--
```agda
{-# OPTIONS --without-K --exact-split --safe #-}

module Setoid.Congruences.Certificates.Congruence where

open import Agda.Primitive using () renaming ( Set to Type )

-- Imports from the Agda Standard Library -----------------------------------
open import Data.Bool.Base                          using  ( if_then_else_ )
open import Data.Empty                              using  ( ⊥ )
open import Data.Fin.Base                           using  ( Fin )
open import Data.Fin.Properties                     using  ( all? )
                                                    renaming ( _≟_ to _≟ᶠ_ )
open import Data.List.Base                          using  ( List ; [] ; _∷_ ; map
                                                           ; filter ; allFin ; foldr )
open import Data.List.Membership.Propositional      using  ( _∈_ ; lose )
open import Data.List.Membership.Propositional.Properties
                                                    using  ( ∈-map⁺ ; ∈-filter⁺
                                                           ; ∈-allFin )

open import Data.List.Relation.Unary.Any            using  ( here ; there )
open import Data.List.Relation.Unary.All            using  ( All ; [] ; _∷_ ; universal )
                                                    renaming  ( lookup to all-lookup
                                                              ; all? to allL? )

open import Data.List.Relation.Unary.All.Properties using  ( map⁺ )
open import Data.Nat.Base                           using  ( ℕ ; zero ; suc )
open import Data.Product                            using  ( _×_ ; _,_ ; proj₁ ; proj₂ )
open import Data.Unit.Base                          using  ( ⊤ ; tt )
open import Data.Vec.Base                           using  ( Vec ; lookup ; tabulate
                                                           ; _[_]≔_ )
                                                    renaming ( map to mapᵥ )
open import Data.Vec.Properties                     using  ( lookup∘tabulate ; lookup∘update
                                                           ; lookup∘update′ ; []≔-idempotent
                                                           ; []≔-lookup ; lookup-map )
open import Function                                using  ( Func )
open import Level                                   using  ( Level ; _⊔_ ; Lift
                                                           ; lift ; lower )
open import Relation.Binary                         using  ( Setoid )
                                                    renaming ( Rel to BinaryRel )

open import Relation.Binary.PropositionalEquality   using  ( _≡_ ; refl ; sym ; trans
                                                           ; cong ; subst ; subst₂ )
open import Relation.Nullary.Decidable              using  ( Dec ; yes ; no ; does ; map′
                                                           ; _×-dec_ ; _→-dec_ ; ¬? )

-- Imports from the Agda Universal Algebra Library ----------------------------
open import Overture                                using  ( 𝓞 ; 𝓥 ; Signature
                                                           ; OperationSymbolsOf
                                                           ; ArityOf )
open import Setoid.Algebras.Basic                   using  ( Algebra ; 𝕌[_]
                                                           ; 𝔻[_] ; _^_ )
open import Setoid.Algebras.Finite                  using  ( FiniteAlgebra )
open import Setoid.Congruences.Basic                using  ( Con ; mkcon ; _∣≈_ )
open import Setoid.Congruences.Finite.Basic         using  ( DecCon )
open import Setoid.Congruences.Generation           using  ( Gen ; Cg ; base ; rfl
                                                           ; symmetric ; transitive
                                                           ; compatible ; Cg-least )
open import Setoid.Congruences.Lattice              using  ( _≑_ )
open import Setoid.Congruences.Presented            using  ( fromPairs ; allVecs
                                                           ; ∈-allVecs )
open import Setoid.Congruences.Certificates.Schema  using  ( ParentVec ; parent
                                                           ; IdempotentParent
                                                           ; forestEdges
                                                           ; Justification ; seed
                                                           ; translate ; mkMerge ; Trace
                                                           ; CgCert )
open import Setoid.Signatures.Finite                using  ( FiniteSignature )

private variable α ρ : Level
```
-->

#### Positional predicates

Trace justifications refer to seed pairs and earlier merges by position.
`AtPos P xs k`{.AgdaFunction} asserts that the element at position `k` of `xs`
exists and satisfies `P` — by recursion on the list, with the out-of-range case
uninhabited, so an invalid reference *is* a failed check rather than a partial
lookup.  `atPos?`{.AgdaFunction} decides it, and `atPos-use`{.AgdaFunction}
consumes it against an `All`{.AgdaDatatype}-package of facts about the same
list (the checker's accumulated `Gen`{.AgdaDatatype} proofs).

```agda
-- The element at position k exists and satisfies P.
AtPos : {a p : Level} {A : Type a} (P : A → Type p) → List A → ℕ → Type p
AtPos {p = p} P []  _        = Lift p ⊥
AtPos P (x ∷ xs)    zero     = P x
AtPos P (x ∷ xs)    (suc k)  = AtPos P xs k

-- AtPos is decidable when P is.
atPos? : {a p : Level} {A : Type a} {P : A → Type p}
  →  ((x : A) → Dec (P x)) → (xs : List A) (k : ℕ) → Dec (AtPos P xs k)
atPos? P? []        k        = no (λ { (lift ()) })
atPos? P? (x ∷ xs)  zero     = P? x
atPos? P? (x ∷ xs)  (suc k)  = atPos? P? xs k

-- Consume a positional fact together with the All-fact at the same position.
atPos-use : {a p q c : Level} {A : Type a}
  {P : A → Type p} {Q : A → Type q} {C : Type c}
  →  (xs : List A) (k : ℕ) → All Q xs → AtPos P xs k
  →  ((x : A) → Q x → P x → C) → C
atPos-use []        k        _           (lift ())
atPos-use (x ∷ xs)  zero     (qx ∷ _)    px  use = use x qx px
atPos-use (x ∷ xs)  (suc k)  (_ ∷ qxs)   pk  use = atPos-use xs k qxs pk use
```

#### The ambient finite finitary algebra

Everything below lives in the named module `CertCheck 𝑭 𝑺`{.AgdaModule},
parameterized by carrier-finiteness data `𝑭` and signature-finiteness data `𝑺`,
so that downstream checkers (and emitted certificate modules) bring the whole
interface into scope with one `open`{.AgdaKeyword}.  As in
[Setoid.Congruences.Presented][], `idx` is a chosen enumeration index for each
carrier element.  `arOf`{.AgdaFunction}
is the arity table against which certificate literals type-check (for concrete
signatures it reduces definitionally), `carrierPairs`{.AgdaFunction} reads an
index-pair list back into the carrier, and `appIdx`{.AgdaFunction} is the
index-level view of one basic-operation application: decode the index tuple,
apply the operation, re-encode.

```agda
module CertCheck {𝑆 : Signature 𝓞 𝓥} {𝑨 : Algebra {𝑆 = 𝑆} α ρ}
                 (𝑭 : FiniteAlgebra 𝑨) (𝑺 : FiniteSignature 𝑆) where

  open FiniteAlgebra 𝑭 using ( _≟_ ; card ; enum ; enum-sur )
  open FiniteSignature 𝑺 using ( opCard ; opEnum ; opEnum-sur
                               ; arCard ; arEnum ; arIdx ; arEnum-arIdx )
  open Setoid 𝔻[ 𝑨 ] using ( _≈_ )
    renaming ( refl to ≈refl ; sym to ≈sym ; trans to ≈trans
             ; reflexive to ≈reflexive )

  private
    -- A chosen enumeration index for each carrier element, and its correctness.
    idx : 𝕌[ 𝑨 ] → Fin card
    idx x = proj₁ (enum-sur x)

    idx-≈ : (x : 𝕌[ 𝑨 ]) → enum (idx x) ≈ x
    idx-≈ x = proj₂ (enum-sur x)

  -- Pairs of enumeration indices: the index-level currency of certificates.
  IdxPair : Type
  IdxPair = Fin card × Fin card

  -- The arity table certificates are checked against.
  arOf : Fin opCard → ℕ
  arOf fi = arCard (opEnum fi)

  -- Reading an index-pair list back into the carrier.
  carrierPairs : List IdxPair → List (𝕌[ 𝑨 ] × 𝕌[ 𝑨 ])
  carrierPairs = map (λ (p₁ , p₂) → enum p₁ , enum p₂)

  -- The carrier tuple encoded by a tuple of carrier indices.
  tupleOf : (fi : Fin opCard)
    → Vec (Fin card) (arOf fi) → (ArityOf 𝑆 (opEnum fi) → 𝕌[ 𝑨 ])
  tupleOf fi t a = enum (lookup t (arIdx (opEnum fi) a))

  -- One basic-operation application, at the index level.
  appIdx : (fi : Fin opCard) → Vec (Fin card) (arOf fi) → Fin card
  appIdx fi t = idx ((opEnum fi ^ 𝑨) (tupleOf fi t))
```

A decidability utility: a universally quantified statement over the index
tuples of one arity is decided by sweeping the tuple enumeration
`allVecs`{.AgdaFunction} of [Setoid.Congruences.Presented][] (whose
completeness `∈-allVecs`{.AgdaFunction} converts the swept
`All`{.AgdaDatatype} back into a Π-statement).

```agda
  -- Decide a Π-statement over index tuples by sweeping the tuple enumeration.
  allVecsΠ? : {p : Level} {k : ℕ} {P : Vec (Fin card) k → Type p}
    →  ((t : Vec (Fin card) k) → Dec (P t)) → Dec (∀ t → P t)
  allVecsΠ? {k = k} {P} P? with allL? P? (allVecs card k)
  ... | yes a  = yes (λ t → all-lookup a (∈-allVecs t))
  ... | no ¬a  = no (λ h → ¬a (universal h (allVecs card k)))
```

#### The claimed partition as a relation

`SameBlock`{.AgdaFunction} is the index-level reading of a parent vector — two
indices related when their parents agree — and `TableRel`{.AgdaFunction} its
carrier-level reading through `idx`, lifted to the working congruence level.

For `TableRel`{.AgdaFunction} to be well defined on the *setoid* carrier the
vector must not distinguish `≈`-equal enumerated elements; that is the
(decidable) `Coherent`{.AgdaFunction} condition, from which respect for `≈`
follows in general (`tableResp-≈`{.AgdaFunction}).

```agda
  -- Two indices lie in the same claimed block.
  SameBlock : ParentVec card → Fin card → Fin card → Type
  SameBlock pv i j = parent pv i ≡ parent pv j

  -- The claimed partition does not distinguish ≈-equal enumerated elements.
  Coherent : ParentVec card → Type ρ
  Coherent pv = ∀ i j → enum i ≈ enum j → SameBlock pv i j

  coherent? : (pv : ParentVec card) → Dec (Coherent pv)
  coherent? pv =
    all? (λ i → all? (λ j → (enum i ≟ enum j) →-dec (parent pv i ≟ᶠ parent pv j)))

  -- The carrier-level relation presented by a parent vector.
  TableRel : ParentVec card → BinaryRel 𝕌[ 𝑨 ] (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ)
  TableRel pv x y = Lift (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ) (SameBlock pv (idx x) (idx y))

  -- The table relation is decidable outright: two lookups and a Fin equality.
  tableDec : (pv : ParentVec card) → ∀ x y → Dec (TableRel pv x y)
  tableDec pv x y = map′ lift lower (parent pv (idx x) ≟ᶠ parent pv (idx y))

  -- ≈-equal elements have same-block indices ...
  sameBlock-resp-≈ : (pv : ParentVec card) → Coherent pv
    →  ∀ {x y} → x ≈ y → SameBlock pv (idx x) (idx y)
  sameBlock-resp-≈ pv coh {x} {y} x≈y =
    coh (idx x) (idx y) (≈trans (idx-≈ x) (≈trans x≈y (≈sym (idx-≈ y))))

  -- ... so the table relation is reflexive over ≈ ...
  tableReflexive : (pv : ParentVec card) → Coherent pv
    →  ∀ {x y} → x ≈ y → TableRel pv x y
  tableReflexive pv coh x≈y = lift (sameBlock-resp-≈ pv coh x≈y)

  -- ... and respects ≈-replacement of related elements.
  tableResp-≈ : (pv : ParentVec card) → Coherent pv
    →  ∀ {x y a b} → x ≈ a → y ≈ b → TableRel pv a b → TableRel pv x y
  tableResp-≈ pv coh x≈a y≈b (lift ab) =
    lift (trans (sameBlock-resp-≈ pv coh x≈a)
                (trans ab (sym (sameBlock-resp-≈ pv coh y≈b))))
```

#### C3, the checked half: one translate step per coordinate

`EdgeCompat`{.AgdaFunction} is the certificate's compatibility obligation: for
every enumerated operation symbol, coordinate, and index tuple, replacing the
coordinate's entry by its *root* stays in the same claimed block.  These are
exactly Freese's unary polynomial translates applied to the forest edges
`(i , parent i)` (a root entry makes the statement trivially reflexive), so the
sweep is linear in the operation-table size.  Everything else about
compatibility is *derived*, not checked.

A simpler design exists and was deliberately rejected: sweeping compatibility
over all *pairs* of pointwise-related tuples would shrink the derivation below
to a few lines, but its decider costs `O(‖A‖²)` where this one is Freese's
`O(r · ‖A‖)` — and linear-cost checking is an acceptance criterion of the
pipeline (#457), not a nicety.  The coordinate walk that follows is the price
of the bound.

```agda
  -- One root-replacement translate step per symbol, coordinate, and tuple.
  EdgeCompat : ParentVec card → Type
  EdgeCompat pv =
    ∀ (fi : Fin opCard) (c : Fin (arOf fi)) (t : Vec (Fin card) (arOf fi))
    → SameBlock pv (appIdx fi t) (appIdx fi (t [ c ]≔ parent pv (lookup t c)))

  edgeCompat? : (pv : ParentVec card) → Dec (EdgeCompat pv)
  edgeCompat? pv =
    all? (λ fi → all? (λ c → allVecsΠ? (λ t →
      parent pv (appIdx fi t) ≟ᶠ
        parent pv (appIdx fi (t [ c ]≔ parent pv (lookup t c))))))
```

The generalization from root-replacement steps to an arbitrary same-block
replacement at one coordinate: detour through the root of each side.

```agda
  -- Replacing one coordinate by a same-block index stays in the same block.
  stepSameBlock : (pv : ParentVec card) → EdgeCompat pv
    →  (fi : Fin opCard) (c : Fin (arOf fi)) (t : Vec (Fin card) (arOf fi))
    →  {a b : Fin card} → SameBlock pv a b
    →  SameBlock pv (appIdx fi (t [ c ]≔ a)) (appIdx fi (t [ c ]≔ b))
  stepSameBlock pv ec fi c t {a} {b} sab =
    trans (toRoot a) (trans mid (sym (toRoot b)))
    where
    -- the EdgeCompat step at entry z, rewritten to a one-shot update
    toRoot : (z : Fin card)
      → SameBlock pv (appIdx fi (t [ c ]≔ z)) (appIdx fi (t [ c ]≔ parent pv z))
    toRoot z = subst
      (λ v → SameBlock pv (appIdx fi (t [ c ]≔ z)) (appIdx fi v))
      (trans (cong (λ w → (t [ c ]≔ z) [ c ]≔ parent pv w) (lookup∘update c t z))
             ([]≔-idempotent t c))
      (ec fi c (t [ c ]≔ z))

    -- the two roots agree, so the two root-updated tuples agree
    mid : SameBlock pv (appIdx fi (t [ c ]≔ parent pv a))
                       (appIdx fi (t [ c ]≔ parent pv b))
    mid = cong (λ z → parent pv (appIdx fi (t [ c ]≔ z))) sab
```

Walking the coordinates.  `overwrite`{.AgdaFunction} replaces the entries of
`t` at a list of coordinates by those of the target `s`;
`overwrite-chain`{.AgdaFunction} shows each replacement preserves the claimed
block of the application (given blockwise-related tuples), and
`overwrite-stable`{.AgdaFunction} / `overwrite-∈`{.AgdaFunction} show a
coordinate once replaced stays replaced, so overwriting *all* coordinates
reaches `s` pointwise.

```agda
  -- Overwrite the entries of t at the listed coordinates with those of s.
  overwrite : {k : ℕ}
    → Vec (Fin card) k → List (Fin k) → Vec (Fin card) k → Vec (Fin card) k
  overwrite t []        s = t
  overwrite t (c ∷ cs)  s = overwrite (t [ c ]≔ lookup s c) cs s

  -- Componentwise same-block relatedness of two index tuples.
  Blockwise : (pv : ParentVec card) {k : ℕ}
    → Vec (Fin card) k → Vec (Fin card) k → Type
  Blockwise pv t s = ∀ q → SameBlock pv (lookup t q) (lookup s q)

  -- Each replacement step preserves the claimed block of the application.
  overwrite-chain : (pv : ParentVec card) → EdgeCompat pv
    →  (fi : Fin opCard) (cs : List (Fin (arOf fi)))
       (t s : Vec (Fin card) (arOf fi))
    →  Blockwise pv t s
    →  SameBlock pv (appIdx fi t) (appIdx fi (overwrite t cs s))
  overwrite-chain pv ec fi []        t s bw = refl
  overwrite-chain pv ec fi (c ∷ cs)  t s bw =
    trans (trans self (stepSameBlock pv ec fi c t (bw c)))
          (overwrite-chain pv ec fi cs (t [ c ]≔ lookup s c) s bw′)
    where
    -- t is its own one-shot update at c
    self : SameBlock pv (appIdx fi t) (appIdx fi (t [ c ]≔ lookup t c))
    self = cong (λ v → parent pv (appIdx fi v)) (sym ([]≔-lookup t c))

    -- the invariant survives the update
    bw′ : Blockwise pv (t [ c ]≔ lookup s c) s
    bw′ q with q ≟ᶠ c
    ... | yes refl = cong (parent pv) (lookup∘update c t (lookup s c))
    ... | no q≢c =
      subst (λ w → SameBlock pv w (lookup s q))
            (sym (lookup∘update′ q≢c t (lookup s c)))
            (bw q)

  -- A coordinate that already agrees with s still agrees after overwriting.
  overwrite-stable : {k : ℕ} (t s : Vec (Fin card) k) (cs : List (Fin k))
    →  (q : Fin k) → lookup t q ≡ lookup s q
    →  lookup (overwrite t cs s) q ≡ lookup s q
  overwrite-stable t s []        q eq = eq
  overwrite-stable t s (c ∷ cs)  q eq with q ≟ᶠ c
  ... | yes refl =
    overwrite-stable _ s cs c (lookup∘update c t (lookup s c))
  ... | no q≢c =
    overwrite-stable _ s cs q (trans (lookup∘update′ q≢c t (lookup s c)) eq)

  -- Overwriting at a listed coordinate lands that coordinate on s.
  overwrite-∈ : {k : ℕ} (t s : Vec (Fin card) k) (cs : List (Fin k)) (q : Fin k)
    →  q ∈ cs → lookup (overwrite t cs s) q ≡ lookup s q
  overwrite-∈ t s (c ∷ cs) .c (here refl) =
    overwrite-stable _ s cs c (lookup∘update c t (lookup s c))
  overwrite-∈ t s (c ∷ cs) q (there w) =
    overwrite-∈ _ s cs q w
```

Compatibility of the table relation.  For an enumerated symbol: encode the two
carrier tuples as index tuples, walk all coordinates with the chain lemma, and
close the gaps — between each carrier tuple and its encoding, and between the
fully overwritten tuple and the target encoding — by `≈`-congruence of the
interpretation plus `Coherent`{.AgdaFunction}.  An arbitrary symbol is an
enumerated one by surjectivity of the symbol enumeration, transported with an
explicit `subst`{.AgdaFunction} on a named motive (the same elaboration-hygiene
device as in [Setoid.Congruences.Presented.Decidable][]).

```agda
  -- The table relation is compatible with every enumerated operation symbol ...
  tableCompatAt : (pv : ParentVec card) → Coherent pv → EdgeCompat pv
    →  (fi : Fin opCard) {u v : ArityOf 𝑆 (opEnum fi) → 𝕌[ 𝑨 ]}
    →  (∀ a → TableRel pv (u a) (v a))
    →  TableRel pv ((opEnum fi ^ 𝑨) u) ((opEnum fi ^ 𝑨) v)
  tableCompatAt pv coh ec fi {u} {v} h =
    lift (trans (sym (encodeSB u)) (trans chain (trans sbOw (encodeSB v))))
    where
    f : OperationSymbolsOf 𝑆
    f = opEnum fi

    -- the index tuple encoding a carrier tuple
    encode : (ArityOf 𝑆 (opEnum fi) → 𝕌[ 𝑨 ]) → Vec (Fin card) (arOf fi)
    encode u′ = tabulate (λ p → idx (u′ (arEnum f p)))

    -- encoding is block-transparent: an encoded tuple is pointwise ≈ its
    -- original (tabulate round trip plus the arity round trip), so their
    -- applications land in the same claimed block
    encodeSB : (u′ : ArityOf 𝑆 (opEnum fi) → 𝕌[ 𝑨 ])
      →  SameBlock pv (appIdx fi (encode u′)) (idx ((f ^ 𝑨) u′))
    encodeSB u′ =
      sameBlock-resp-≈ pv coh (Func.cong (Algebra.Interp 𝑨) (refl , enc≈))
      where
      enc≈ : ∀ a → tupleOf fi (encode u′) a ≈ u′ a
      enc≈ a = ≈trans
        (≈reflexive (cong enum
          (trans (lookup∘tabulate (λ q → idx (u′ (arEnum f q))) (arIdx f a))
                 (cong (λ b → idx (u′ b)) (arEnum-arIdx f a)))))
        (idx-≈ (u′ a))

    tu tv : Vec (Fin card) (arOf fi)
    tu = encode u
    tv = encode v

    -- the encodings are blockwise related, by the hypothesis
    bw : Blockwise pv tu tv
    bw p = subst₂ (SameBlock pv)
                  (sym (lookup∘tabulate (λ q → idx (u (arEnum f q))) p))
                  (sym (lookup∘tabulate (λ q → idx (v (arEnum f q))) p))
                  (lower (h (arEnum f p)))

    -- walking every coordinate turns tu into tv, blockwise
    chain : SameBlock pv (appIdx fi tu)
                         (appIdx fi (overwrite tu (allFin (arOf fi)) tv))
    chain = overwrite-chain pv ec fi (allFin (arOf fi)) tu tv bw

    -- the fully overwritten tuple is pointwise tv
    sbOw : SameBlock pv (appIdx fi (overwrite tu (allFin (arOf fi)) tv))
                        (appIdx fi tv)
    sbOw = sameBlock-resp-≈ pv coh
      (Func.cong (Algebra.Interp 𝑨)
        (refl , λ a → ≈reflexive (cong enum
          (overwrite-∈ tu tv (allFin (arOf fi)) (arIdx f a) (∈-allFin (arIdx f a))))))

  -- ... hence with every operation symbol, by surjectivity of the enumeration.
  private
    TableCompatMotive : ParentVec card → OperationSymbolsOf 𝑆
      → Type (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ)
    TableCompatMotive pv g = {u v : ArityOf 𝑆 g → 𝕌[ 𝑨 ]}
      →  (∀ a → TableRel pv (u a) (v a))
      →  TableRel pv ((g ^ 𝑨) u) ((g ^ 𝑨) v)

  tableCompat : (pv : ParentVec card) → Coherent pv → EdgeCompat pv
    →  𝑨 ∣≈ TableRel pv
  tableCompat pv coh ec f =
    subst (TableCompatMotive pv) (proj₂ (opEnum-sur f))
          (tableCompatAt pv coh ec (proj₁ (opEnum-sur f)))
```

The claimed partition is therefore a congruence — packaged with its
decision procedure as a `DecCon`{.AgdaFunction} whose decider is two lookups,
never a closure computation.

```agda
  -- The claimed partition as a congruence at the working level ...
  tableCon : (pv : ParentVec card) → Coherent pv → EdgeCompat pv
    →  Con 𝑨 (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ)
  tableCon pv coh ec = TableRel pv , mkcon
    (tableReflexive pv coh)
    (record { refl   = lift refl
            ; sym    = λ e → lift (sym (lower e))
            ; trans  = λ e₁ e₂ → lift (trans (lower e₁) (lower e₂)) })
    (tableCompat pv coh ec)

  -- ... and as a decidable congruence.
  tableDecCon : (pv : ParentVec card) → Coherent pv → EdgeCompat pv
    →  DecCon 𝑨 (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ)
  tableDecCon pv coh ec = tableCon pv coh ec , tableDec pv
```

#### C3, concluded: the generated congruence is contained in the claim

The seed pairs must land in the claimed blocks — the decidable
`Respects`{.AgdaFunction} sweep — and then `Cg-least`{.AgdaFunction} contains
the whole generated congruence in the table congruence.

```agda
  -- Every listed pair is same-block.
  Respects : ParentVec card → List IdxPair → Type
  Respects pv ps = All (λ p → SameBlock pv (proj₁ p) (proj₂ p)) ps

  respects? : (pv : ParentVec card) (ps : List IdxPair) → Dec (Respects pv ps)
  respects? pv ps = allL? (λ p → parent pv (proj₁ p) ≟ᶠ parent pv (proj₂ p)) ps

  -- The presented relation of a respected seed list is contained in the
  -- claim: walk the list to the presenting pair; its endpoints' chosen
  -- indices share the listed pair's blocks by coherence.
  fromPairs-table-⊆ : (pv : ParentVec card) (ps : List IdxPair)
    →  Coherent pv → Respects pv ps
    →  ∀ {x y} → fromPairs {𝑨 = 𝑨} (carrierPairs ps) x y → TableRel pv x y
  fromPairs-table-⊆ pv []       coh []          ()
  fromPairs-table-⊆ pv (p ∷ ps) coh (sb ∷ _)    (here (x≈ , y≈)) =
    tableResp-≈ pv coh x≈ y≈
      (lift (trans (bridge (proj₁ p)) (trans sb (sym (bridge (proj₂ p))))))
    where
    -- the chosen index of an enumerated element shares its block
    bridge : (i : Fin card) → parent pv (idx (enum i)) ≡ parent pv i
    bridge i = coh (idx (enum i)) i (idx-≈ (enum i))
  fromPairs-table-⊆ pv (p ∷ ps) coh (_ ∷ rsp)   (there mem) =
    fromPairs-table-⊆ pv ps coh rsp mem

  -- C3: the generated congruence of a respected seed list is contained in
  -- the claimed congruence (by the congruence generation theorem).
  Cg⊑table : (pv : ParentVec card) (ps : List IdxPair)
    →  (coh : Coherent pv) (ec : EdgeCompat pv) → Respects pv ps
    →  ∀ {x y} → Gen {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs ps)) x y
    →  TableRel pv x y
  Cg⊑table pv ps coh ec rsp =
    Cg-least (tableCon pv coh ec) (fromPairs-table-⊆ pv ps coh rsp)
```

The forest edges of an idempotent vector are respected by that vector itself —
each edge relates an index to its own root — so for the seed list
`forestEdges pv` the `Respects`{.AgdaFunction} obligation is free.

```agda
  -- A vector respects its own forest edges.
  edgesRespected : (pv : ParentVec card) → IdempotentParent pv
    →  Respects pv (forestEdges pv)
  edgesRespected pv idem =
    map⁺ (universal (λ i → sym (idem i))
                    (filter (λ i → ¬? (i ≟ᶠ parent pv i)) (allFin card)))
```

#### C1: trace soundness

Fix a seed list `ps`.  `GenPair ps`{.AgdaFunction} is membership of an index
pair in the generated congruence; `JustOK`{.AgdaFunction} is the validity of
one justification against the seed list and the already-processed merges
(most-recent-first, per the schema's reference conventions), stated through
`AtPos`{.AgdaFunction} so that decidability and consumption are both structural.

```agda
  -- Membership of an index pair in the congruence generated by the seeds.
  GenPair : List IdxPair → IdxPair → Type (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ)
  GenPair ps p =
    Gen {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs ps))
        (enum (proj₁ p)) (enum (proj₂ p))

  -- Validity of one justification for merging (i , j).
  JustOK : (ps done : List IdxPair) (i j : Fin card)
    →  Justification card opCard arOf → Type ρ
  JustOK ps done i j (seed s) =
    AtPos (λ p → (enum i ≈ enum (proj₁ p)) × (enum j ≈ enum (proj₂ p))) ps s
  JustOK ps done i j (translate fi c w r) =
    AtPos (λ p → (enum i ≈ (opEnum fi ^ 𝑨) (tupleOf fi (w [ c ]≔ proj₁ p)))
               × (enum j ≈ (opEnum fi ^ 𝑨) (tupleOf fi (w [ c ]≔ proj₂ p))))
          done r

  justOK? : (ps done : List IdxPair) (i j : Fin card)
    →  (ju : Justification card opCard arOf) → Dec (JustOK ps done i j ju)
  justOK? ps done i j (seed s) =
    atPos? (λ p → (enum i ≟ enum (proj₁ p)) ×-dec (enum j ≟ enum (proj₂ p))) ps s
  justOK? ps done i j (translate fi c w r) =
    atPos? (λ p → (enum i ≟ (opEnum fi ^ 𝑨) (tupleOf fi (w [ c ]≔ proj₁ p)))
             ×-dec (enum j ≟ (opEnum fi ^ 𝑨) (tupleOf fi (w [ c ]≔ proj₂ p))))
           done r
```

A valid trace is a run of valid justifications, each against the merges before
it; `merges`{.AgdaFunction} is the final accumulator.  Both are single
structural folds, as is the decider.

```agda
  -- Validity of a trace, processing merges into the accumulator done.
  TraceValidFrom : (ps done : List IdxPair)
    →  Trace card opCard arOf → Type ρ
  TraceValidFrom ps done [] = Lift ρ ⊤
  TraceValidFrom ps done (mkMerge i j ju ∷ tr) =
    JustOK ps done i j ju × TraceValidFrom ps ((i , j) ∷ done) tr

  traceValidFrom? : (ps done : List IdxPair) (tr : Trace card opCard arOf)
    →  Dec (TraceValidFrom ps done tr)
  traceValidFrom? ps done [] = yes (lift tt)
  traceValidFrom? ps done (mkMerge i j ju ∷ tr) =
    justOK? ps done i j ju ×-dec traceValidFrom? ps ((i , j) ∷ done) tr

  TraceValid : List IdxPair → Trace card opCard arOf → Type ρ
  TraceValid ps tr = TraceValidFrom ps [] tr

  traceValid? : (ps : List IdxPair) (tr : Trace card opCard arOf)
    →  Dec (TraceValid ps tr)
  traceValid? ps tr = traceValidFrom? ps [] tr

  -- The merged pairs of a trace, most recent first.
  mergesFrom : List IdxPair → Trace card opCard arOf → List IdxPair
  mergesFrom done []                     = done
  mergesFrom done (mkMerge i j _ ∷ tr)  = mergesFrom ((i , j) ∷ done) tr

  merges : Trace card opCard arOf → List IdxPair
  merges = mergesFrom []
```

A valid seed justification is `Any`-membership of the pair in the presented
relation — recovered structurally, at the recorded position.

```agda
  -- A valid seed reference presents the merged pair.
  seedAt : (ps : List IdxPair) (s : ℕ) {i j : Fin card}
    →  AtPos (λ p → (enum i ≈ enum (proj₁ p)) × (enum j ≈ enum (proj₂ p))) ps s
    →  fromPairs {𝑨 = 𝑨} (carrierPairs ps) (enum i) (enum j)
  seedAt []        s        (lift ())
  seedAt (p ∷ ps)  zero     ok = here ok
  seedAt (p ∷ ps)  (suc s)  ok = there (seedAt ps s ok)
```

One valid justification yields one `Gen`{.AgdaDatatype} derivation: a seed by
the `base`{.AgdaInductiveConstructor} rule; a translate by one
`compatible`{.AgdaInductiveConstructor} rule applied to the earlier merge at
the moving coordinate and to reflexivity at the frozen coordinates, wrapped in
the recorded `≈`-matches.  This is obligation C1, entry by entry.

```agda
  -- C1, one entry: a valid justification derives its merged pair.
  justGen : (ps done : List IdxPair) {i j : Fin card}
    →  (ju : Justification card opCard arOf)
    →  All (GenPair ps) done → JustOK ps done i j ju → GenPair ps (i , j)
  justGen ps done (seed s) dall ok = base (seedAt ps s ok)
  justGen ps done {i} {j} (translate fi c w r) dall ok =
    atPos-use done r dall ok derive
    where
    f : OperationSymbolsOf 𝑆
    f = opEnum fi

    derive : (p : IdxPair) → GenPair ps p
      →  (enum i ≈ (f ^ 𝑨) (tupleOf fi (w [ c ]≔ proj₁ p)))
       × (enum j ≈ (f ^ 𝑨) (tupleOf fi (w [ c ]≔ proj₂ p)))
      →  GenPair ps (i , j)
    derive (x , y) gxy (ei≈ , ej≈) =
      transitive (rfl ei≈)
        (transitive (compatible f ptw) (symmetric (rfl ej≈)))
      where
      R : BinaryRel 𝕌[ 𝑨 ] (α ⊔ ρ)
      R = fromPairs {𝑨 = 𝑨} (carrierPairs ps)

      -- the two frozen tuples are pointwise generated-related:
      -- the moving coordinate by the earlier merge, the rest by reflexivity
      ptw : ∀ a → Gen {𝑨 = 𝑨} R (tupleOf fi (w [ c ]≔ x) a)
                                (tupleOf fi (w [ c ]≔ y) a)
      ptw a with arIdx f a ≟ᶠ c
      ... | yes p =
        subst₂ (λ s′ t′ → Gen {𝑨 = 𝑨} R (enum s′) (enum t′))
               (sym (trans (cong (lookup (w [ c ]≔ x)) p) (lookup∘update c w x)))
               (sym (trans (cong (lookup (w [ c ]≔ y)) p) (lookup∘update c w y)))
               gxy
      ... | no ¬p =
        subst₂ (λ s′ t′ → Gen {𝑨 = 𝑨} R (enum s′) (enum t′))
               (sym (lookup∘update′ ¬p w x))
               (sym (lookup∘update′ ¬p w y))
               (rfl ≈refl)
```

C1, the whole trace: fold the entries, accumulating each derived pair.

```agda
  -- C1: every merged pair of a valid trace is generated.
  traceGenFrom : (ps done : List IdxPair) (tr : Trace card opCard arOf)
    →  All (GenPair ps) done → TraceValidFrom ps done tr
    →  All (GenPair ps) (mergesFrom done tr)
  traceGenFrom ps done [] dall _ = dall
  traceGenFrom ps done (mkMerge i j ju ∷ tr) dall (ok , rest) =
    traceGenFrom ps ((i , j) ∷ done) tr (justGen ps done ju dall ok ∷ dall) rest

  traceGen : (ps : List IdxPair) (tr : Trace card opCard arOf)
    →  TraceValid ps tr → All (GenPair ps) (merges tr)
  traceGen ps tr tv = traceGenFrom ps [] tr [] tv
```

#### C2: replaying the merges

The replay state is a root vector, initially the identity.  Processing one
merged pair re-points every index rooted at the right root to the left root —
the eager, proofless core of a union-find, adequate because the checker replays
a *given* ≤ `n − 1`-entry list exactly once.  (`merges`{.AgdaFunction} is
most-recent-first, and `foldr`{.AgdaFunction} therefore applies the *head*
last: the replay processes the trace in run order.)

```agda
  -- Re-point one root: entries rooted at rv move to ru.
  repoint : Fin card → Fin card → Fin card → Fin card
  repoint ru rv r = if does (r ≟ᶠ rv) then ru else r

  -- Process one merged pair.
  replayStep : Vec (Fin card) card → IdxPair → Vec (Fin card) card
  replayStep st p =
    mapᵥ (repoint (lookup st (proj₁ p)) (lookup st (proj₂ p))) st

  -- Replay a merge list from the identity partition.
  replayRoots : List IdxPair → Vec (Fin card) card
  replayRoots ms = foldr (λ p st → replayStep st p) (tabulate (λ i → i)) ms
```

The soundness invariant: every index is generated-related to its current
replay root.  It holds initially by reflexivity and is preserved by each step —
the re-pointed indices reach their new root through the merged pair.

```agda
  -- Every index is generated-related to its replay root.
  ReplaySound : List IdxPair → Vec (Fin card) card → Type (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ)
  ReplaySound ps st = ∀ i → GenPair ps (i , lookup st i)

  -- Both containments of the claim in a generated congruence have the same
  -- shape: pass from the carrier pair to its chosen indices, walk each index
  -- (generated-relatedly) to a representative, and cross the gap with the
  -- given equality of representatives.  Stated once, used for the replay
  -- roots below and for the parent pointers in the trace-free case.
  private
    viaReps : (ps : List IdxPair) (f : Fin card → Fin card)
      →  (walk : ∀ i → GenPair ps (i , f i))
      →  ∀ {x y} → f (idx x) ≡ f (idx y)
      →  Gen {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs ps)) x y
    viaReps ps f walk {x} {y} eq =
      transitive (symmetric (rfl (idx-≈ x)))
        (transitive (walk (idx x))
          (transitive (rfl (≈reflexive (cong enum eq)))
            (transitive (symmetric (walk (idx y))) (rfl (idx-≈ y)))))

  private
    -- one re-pointed entry, with the decision exposed as an argument
    repoint-gen : (ps : List IdxPair) {ru rv : Fin card} (r : Fin card)
      →  (d : Dec (r ≡ rv)) {i : Fin card}
      →  GenPair ps (i , r) → GenPair ps (rv , ru)
      →  GenPair ps (i , (if does d then ru else r))
    repoint-gen ps r (yes q) g h =
      transitive g (subst (λ z → GenPair ps (z , _)) (sym q) h)
    repoint-gen ps r (no _)  g _ = g

  -- One step preserves the invariant.
  replayStep-sound : (ps : List IdxPair) (st : Vec (Fin card) card)
    →  (p : IdxPair) → GenPair ps p → ReplaySound ps st
    →  ReplaySound ps (replayStep st p)
  replayStep-sound ps st (u , v) guv snd i =
    subst (λ z → GenPair ps (i , z))
          (sym (lookup-map i (repoint (lookup st u) (lookup st v)) st))
          (repoint-gen ps (lookup st i) (lookup st i ≟ᶠ lookup st v)
                       (snd i) rv→ru)
    where
    -- from the old right root to the old left root, through the merged pair
    rv→ru : GenPair ps (lookup st v , lookup st u)
    rv→ru = transitive (symmetric (snd v))
                       (transitive (symmetric guv) (snd u))

  -- The invariant holds after replaying a generated merge list.
  replay-sound : (ps ms : List IdxPair)
    →  All (GenPair ps) ms → ReplaySound ps (replayRoots ms)
  replay-sound ps [] [] i =
    subst (λ z → GenPair ps (i , z))
          (sym (lookup∘tabulate (λ j → j) i)) (rfl ≈refl)
  replay-sound ps (p ∷ ms) (g ∷ gs) =
    replayStep-sound ps (replayRoots ms) p g (replay-sound ps ms gs)
```

The alignment condition `Covers`{.AgdaFunction}: the replayed roots are
constant along the claimed parent pointers.  One linear sweep, and exactly what
the containment argument consumes — if two indices share a claimed parent, they
share a replayed root, hence both are generated-related to it.  (No converse
sweep is needed: the *other* inclusion is C3, and an over-merging trace would
merely make the two checks jointly unsatisfiable, never unsound.)

```agda
  -- The replayed roots are constant along the claimed parent pointers.
  Covers : ParentVec card → Vec (Fin card) card → Type
  Covers pv rr = ∀ i → lookup rr (parent pv i) ≡ lookup rr i

  covers? : (pv : ParentVec card) (rr : Vec (Fin card) card)
    →  Dec (Covers pv rr)
  covers? pv rr = all? (λ i → lookup rr (parent pv i) ≟ᶠ lookup rr i)

  -- C2: the claimed congruence is contained in the generated one.
  table⊑Cg : (pv : ParentVec card) (ps : List IdxPair)
    →  (tr : Trace card opCard arOf)
    →  TraceValid ps tr → Covers pv (replayRoots (merges tr))
    →  ∀ {x y} → TableRel pv x y
    →  Gen {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs ps)) x y
  table⊑Cg pv ps tr tv cov {x} {y} (lift same) =
    viaReps ps (lookup rr) (replay-sound ps (merges tr) (traceGen ps tr tv)) key
    where
    rr : Vec (Fin card) card
    rr = replayRoots (merges tr)

    -- same claimed parent forces same replayed root
    key : lookup rr (idx x) ≡ lookup rr (idx y)
    key = trans (sym (cov (idx x)))
                (trans (cong (lookup rr) same) (cov (idx y)))
```

#### The trace-free special case: a vector generates itself from its edges

When the seed list is the vector's *own* forest edges, no trace is needed: an
index reaches its root in one edge (or is a root), so the containment of the
claim in the generated congruence is direct.  This is the form the
whole-lattice checker uses for every listed congruence.

```agda
  -- Every index is edge-generated-related to its root.
  toRootGen : (pv : ParentVec card) (i : Fin card)
    →  Gen {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs (forestEdges pv)))
           (enum i) (enum (parent pv i))
  toRootGen pv i with i ≟ᶠ parent pv i
  ... | yes q = rfl (≈reflexive (cong enum q))
  ... | no ¬q = base (lose mem (≈refl , ≈refl))
    where
    mem : (enum i , enum (parent pv i)) ∈ carrierPairs (forestEdges pv)
    mem = ∈-map⁺ (λ p → enum (proj₁ p) , enum (proj₂ p))
            (∈-map⁺ (λ a → a , parent pv a)
              (∈-filter⁺ (λ a → ¬? (a ≟ᶠ parent pv a)) (∈-allFin i) ¬q))

  -- The claimed congruence is contained in the one its edges generate.
  table⊑CgEdges : (pv : ParentVec card)
    →  ∀ {x y} → TableRel pv x y
    →  Gen {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs (forestEdges pv))) x y
  table⊑CgEdges pv (lift same) =
    viaReps (forestEdges pv) (parent pv) (toRootGen pv) same
```

#### The headline theorems

Both directions, packaged as an honest `_≑_`{.AgdaFunction} at the working
congruence level: with a trace, for an arbitrary seed list; and trace-free,
for a vector against its own forest edges.

```agda
  -- θ ≑ Cg (fromPairs P), from a checked certificate.
  table≑Cg : (pv : ParentVec card) (ps : List IdxPair)
    →  (tr : Trace card opCard arOf)
    →  (coh : Coherent pv) (ec : EdgeCompat pv)
    →  Respects pv ps → TraceValid ps tr
    →  Covers pv (replayRoots (merges tr))
    →  tableCon pv coh ec ≑ Cg {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs ps))
  table≑Cg pv ps tr coh ec rsp tv cov =
    table⊑Cg pv ps tr tv cov , Cg⊑table pv ps coh ec rsp

  -- θ ≑ Cg (its own forest edges), with no trace at all.
  table≑CgEdges : (pv : ParentVec card)
    →  (coh : Coherent pv) (ec : EdgeCompat pv) → IdempotentParent pv
    →  tableCon pv coh ec
         ≑ Cg {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs (forestEdges pv)))
  table≑CgEdges pv coh ec idem =
    table⊑CgEdges pv , Cg⊑table pv (forestEdges pv) coh ec (edgesRespected pv idem)
```

Finally, the bundled interface for one standalone certificate: the conjunction
of all five checked conditions, its decider (one decision for the whole
certificate), and the soundness theorem consuming it.

```agda
  -- All checked conditions of one per-congruence certificate.
  CgCertOK : CgCert card opCard arOf → Type ρ
  CgCertOK cc =
    Coherent part × EdgeCompat part × Respects part seeds
      × TraceValid seeds trace × Covers part (replayRoots (merges trace))
    where open CgCert cc

  cgCertOK? : (cc : CgCert card opCard arOf) → Dec (CgCertOK cc)
  cgCertOK? cc =
    coherent? part ×-dec edgeCompat? part ×-dec respects? part seeds
      ×-dec traceValid? seeds trace ×-dec covers? part (replayRoots (merges trace))
    where open CgCert cc

  -- The certificate's claim, from its checked conditions.
  cgCertSound : (cc : CgCert card opCard arOf) (ok : CgCertOK cc)
    →  tableCon (CgCert.part cc) (proj₁ ok) (proj₁ (proj₂ ok))
         ≑ Cg {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs (CgCert.seeds cc)))
  cgCertSound cc (coh , ec , rsp , tv , cov) =
    table≑Cg (CgCert.part cc) (CgCert.seeds cc) (CgCert.trace cc)
             coh ec rsp tv cov
```

--------------------------------------

[^1]: [PR #467](https://github.com/ualib/agda-algebras/pull/467)