---
layout: default
file: "src/Setoid/Congruences/Finite/Decidable.lagda.md"
title: "Setoid.Congruences.Finite.Decidable module (The Agda Universal Algebra Library)"
date: "2026-07-12"
author: "the agda-algebras development team"
---
### Constructive completeness of the decidable congruence layer
This is the [Setoid.Congruences.Finite.Decidable][] module of the [Agda Universal Algebra Library][].
[Setoid.Congruences.Finite.Basic][] defines the congruence-side finiteness interface
`FiniteCongruences`{.AgdaRecord}, whose `complete`{.AgdaField} field asserts that a
finite list of decidable congruences exhausts the *whole* congruence lattice up to `≑`.
That field quantifies over *all* semantic congruences `Con`{.AgdaFunction}, and the
non-constructivity ("no-go") theorem shows it carries genuine classical content (its
strength sits between weak excluded middle and excluded middle).[^1]
This module supplies the *constructive* counterpart.[^2] It builds, from a
`FiniteAlgebra`{.AgdaRecord} ([Setoid.Algebras.Finite][]) and a
`FiniteSignature`{.AgdaRecord} ([Setoid.Signatures.Finite][]) alone, a finite list of
`DecCon`{.AgdaFunction}s that is complete for `DecCon`{.AgdaFunction} — every
*decidable* congruence is `≑` to a listed one — with **no classical axiom**.
The resulting interface record is `FiniteCongruencesᵈ`{.AgdaRecord}, the
decidable-layer sibling of `FiniteCongruences`{.AgdaRecord}, identical in shape, but
its completeness field `completeᵈ`{.AgdaField} quantifies only over
`DecCon`{.AgdaFunction}, which is exactly why it can be *proved* rather than assumed.
The two records are genuinely distinct interfaces — they differ in the domain of
quantification, `DecCon`{.AgdaFunction} versus `Con`{.AgdaFunction} — and are not
synonyms.[^3]
#### The construction, and how it reuses slices L1 and L2
A `DecCon`{.AgdaFunction} on a finite carrier is determined, up to `≑`, by the
`card`{.AgdaField} `×` `card`{.AgdaField} grid of its decisions on enumerated
elements: two decidable congruences that agree on `enum i , enum j` for all indices
are mutually contained, because the enumeration is surjective and congruences
respect `≈`. So enumerating all such grids enumerates all decidable congruences up
to `≑`. A grid is a Boolean matrix, represented here as a `Vec`{.AgdaDatatype} of
`Vec`{.AgdaDatatype}s of `Bool`{.AgdaDatatype}, and `allGrids`{.AgdaFunction} lists
all `2 ^ (card ²)` of them; `∈-allGrids`{.AgdaFunction} is the completeness of that
enumeration.
Each grid is decoded to a `DecCon`{.AgdaFunction} by **generating** the congruence of
its kept pairs: `decode V = Cg-DecCon (gpairs V)`, where `gpairs V`{.AgdaFunction}
lists the enumerated pairs the matrix turns on, and `Cg-DecCon`{.AgdaFunction} —
Lemma L1 of [Setoid.Congruences.Presented.Decidable][] — packages the congruence
generated by a finite pair list as a `DecCon`{.AgdaFunction}, already carrying its
own decision procedure.
(In the code `decode`{.AgdaFunction} splits this into a transparent underlying
congruence `decodeCon`{.AgdaFunction} and an `abstract` decision procedure
`decodeDec`{.AgdaFunction}, so the enormous symbolic congruence-closure term L1's
decider carries is never normalized into a completeness goal — the elaboration-cost
analogue of L1's own `with`-normalization caution.)
This is a deliberate deviation from the design note's suggested recipe of *filtering*
the matrices to congruences and decoding each to a raw Boolean-lookup relation:
filtering is unnecessary because `Cg`{.AgdaFunction} of *any* pair list is already
a congruence, so decoding through `Cg-DecCon`{.AgdaFunction} reuses all of L1's
soundness, completeness, and compatibility work as a black box instead of re-deriving
operation-compatibility for an arbitrary matrix fixpoint.
Completeness is then the reconstruction argument of L2
([Setoid.Congruences.Presented.Basic][]), specialized to the matrix-derived list: for
a `DecCon`{.AgdaFunction} `d`, its own grid `gridOf d` is in `allGrids`{.AgdaFunction},
and `proj₁ d ≑ proj₁ (decode (gridOf d))` holds because the pairs `gpairs (gridOf d)`
keeps are exactly the `d`-related enumerated pairs.
The two containments are the `base`{.AgdaInductiveConstructor} rule of
`Cg`{.AgdaFunction} (`d` is contained in the generated congruence) and
`Cg-least`{.AgdaFunction} (the generated congruence is contained in `d`), assembled
from `con-resp-≈`{.AgdaFunction} of [Setoid.Congruences.Presented.Basic][] exactly as in
`reconstruction`{.AgdaFunction} of L2 — matching `gpairs (gridOf d)` to `relatedPairs d`
as lists would require filter/map-fusion lemmas, so we re-run the two-inclusion pattern
of L2 on the matrix-derived list rather than transport its theorem.[^4]
<!--
```agda
{-# OPTIONS --cubical-compatible --exact-split --safe #-}
module Setoid.Congruences.Finite.Decidable where
open import Agda.Primitive using () renaming ( Set to Type )
open import Data.Bool.Base using ( Bool ; true
; false ; T )
open import Data.Fin.Base using ( Fin ; zero ; suc )
open import Data.List.Base using ( List ; [] ; _∷_
; map ; filter ; allFin
; concatMap
; cartesianProduct )
open import Data.List.Membership.Propositional using ( _∈_ ; lose )
open import Data.List.Membership.Propositional.Properties using ( ∈-map⁺ ; ∈-filter⁺
; ∈-concat⁺′ ; ∈-allFin
; ∈-cartesianProduct⁺ )
open import Data.List.Relation.Unary.All using ( All ; lookupAny )
renaming ( map to all-map )
open import Data.List.Relation.Unary.All.Properties using ( all-filter ; map⁺ )
open import Data.List.Relation.Unary.Any using ( here ; there )
open import Data.Nat.Base using ( ℕ ; zero ; suc )
open import Data.Product using ( _×_ ; _,_ ; proj₁
; proj₂ ; Σ-syntax )
open import Data.Vec.Base using ( Vec ; [] ; _∷_
; lookup ; tabulate )
open import Data.Vec.Properties using ( lookup∘tabulate )
open import Function using ( _∘_ )
open import Level using ( Level ; _⊔_ )
renaming ( suc to lsuc )
open import Relation.Binary using ( Setoid )
open import Relation.Binary.PropositionalEquality using ( cong ; refl ; sym
; _≡_ ; trans ; subst )
open import Relation.Nullary.Decidable using ( Dec ; does ; T? )
open import Overture using ( 𝓞 ; 𝓥 ; Signature ; 𝑆 )
open import Setoid.Algebras.Basic using ( Algebra ; 𝕌[_] ; 𝔻[_] )
open import Setoid.Algebras.Finite using ( FiniteAlgebra )
open import Setoid.Congruences.Basic using ( Con )
open import Setoid.Congruences.Finite.Basic using ( DecCon ; ConRel )
open import Setoid.Congruences.Generation using ( Cg ; Gen ; base ; Cg-least )
open import Setoid.Congruences.Lattice using ( _≑_ )
open import Setoid.Congruences.Presented using ( fromPairs ; con-resp-≈
; Cg-DecCon ; does-in ; does-out )
open import Setoid.Signatures.Finite using ( FiniteSignature )
private variable α ρ ℓ : Level
```
-->
#### The Layer-D congruence interface
`FiniteCongruencesᵈ`{.AgdaRecord} `𝑨` bundles a finite list `consᵈ`{.AgdaField} of
decidable congruences with a proof `completeᵈ`{.AgdaField} that the list exhausts the
*decidable* congruences of `𝑨` up to `≑`. Contrast with
`FiniteCongruences`{.AgdaRecord} of [Setoid.Congruences.Finite.Basic][]: that record's
`complete`{.AgdaField} field ranges over every `Con`{.AgdaFunction} (Layer S, the
classical bridge), whereas `completeᵈ`{.AgdaField} ranges only over
`DecCon`{.AgdaFunction} (Layer D), which is what makes it constructively provable
below. The `witnessᵈ*`{.AgdaFunction} projections mirror the `witness*` helpers of
the semantic record.
```agda
record FiniteCongruencesᵈ {𝑆 : Signature 𝓞 𝓥}(𝑨 : Algebra {𝑆 = 𝑆} α ρ) : Type (lsuc (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ)) where
field
consᵈ : List (DecCon 𝑨 (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ))
completeᵈ : ∀ d → Σ[ e ∈ DecCon 𝑨 (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ) ] (e ∈ consᵈ) × (proj₁ d ≑ proj₁ e)
witnessᵈ : DecCon 𝑨 (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ) → DecCon 𝑨 (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ)
witnessᵈ = proj₁ ∘ completeᵈ
witnessᵈ∈ : ∀ d → witnessᵈ d ∈ consᵈ
witnessᵈ∈ = proj₁ ∘ proj₂ ∘ completeᵈ
witnessᵈ≑ : ∀ d → proj₁ d ≑ proj₁ (witnessᵈ d)
witnessᵈ≑ = proj₂ ∘ proj₂ ∘ completeᵈ
```
#### Enumerating vectors over a finite list
The matrix enumeration is built from one generic, signature-agnostic tool:
`listVecs xs k`{.AgdaFunction} lists every length-`k` `Vec`{.AgdaDatatype} whose
entries are drawn from the list `xs`, and `∈-listVecs`{.AgdaFunction} is its
completeness — a vector all of whose entries occur in `xs` occurs in the list. This
is the `Data.List`-analogue of `allVecs`{.AgdaFunction} of
[Setoid.Congruences.Presented.Decidable][], generalized from `allFin`{.AgdaFunction}
to an arbitrary source list; keeping the entries as honest inductive data (rather
than functions out of `Fin`{.AgdaDatatype}) is what lets membership be stated up to
propositional `_≡_` with no appeal to function extensionality.
```agda
listVecs : {A : Type ℓ} → List A → (k : ℕ) → List (Vec A k)
listVecs xs zero = [] ∷ []
listVecs xs (suc k) = concatMap (λ a → map (a ∷_) (listVecs xs k)) xs
∈-listVecs : {A : Type ℓ}(xs : List A){k : ℕ}(v : Vec A k)
→ (∀ p → lookup v p ∈ xs) → v ∈ listVecs xs k
∈-listVecs xs [] _ = here refl
∈-listVecs xs {suc k}(a ∷ v) h =
∈-concat⁺′ (∈-map⁺ (a ∷_) (∈-listVecs xs v (λ p → h (suc p))))
(∈-map⁺ (λ b → map (b ∷_) (listVecs xs k)) (h zero))
```
The source list of a single bit is `true ∷ false ∷ []`, complete for
`Bool`{.AgdaDatatype}.
```agda
allBits : List Bool
allBits = true ∷ false ∷ []
∈-allBits : (b : Bool) → b ∈ allBits
∈-allBits true = here refl
∈-allBits false = there (here refl)
```
#### The enumeration of decidable congruences
Fix a finite finitary algebra: an algebra `𝑨` with carrier-finiteness data `𝑭` and
signature-finiteness data `𝑺`. Only `card`{.AgdaField}, `enum`{.AgdaField}, and
`enum-sur`{.AgdaField} of `𝑭` are used directly here; the `_≟_`{.AgdaField} field and
all of `𝑺` enter only through `Cg-DecCon`{.AgdaFunction}.
```agda
module _ {𝓞 𝓥 : Level}{𝑆 : Signature 𝓞 𝓥}{𝑨 : Algebra {𝑆 = 𝑆} α ρ}(𝑭 : FiniteAlgebra 𝑨)(𝑺 : FiniteSignature 𝑆) where
open FiniteAlgebra 𝑭 using ( card ; enum ; enum-sur )
open Setoid 𝔻[ 𝑨 ] using ( _≈_ ) renaming ( sym to ≈sym )
private
idx : 𝕌[ 𝑨 ] → Fin card
idx x = proj₁ (enum-sur x)
idx-≈ : (x : 𝕌[ 𝑨 ]) → enum (idx x) ≈ x
idx-≈ x = proj₂ (enum-sur x)
```
A **grid** is a Boolean matrix over the carrier enumeration, stored as a vector of
rows; `entryOf V i j`{.AgdaFunction} reads the `(i , j)` bit. The enumeration
`allGrids`{.AgdaFunction} lists every grid, and `∈-allGrids`{.AgdaFunction} is its
completeness, both by two applications of `listVecs`{.AgdaFunction}.
```agda
Grid : Type
Grid = Vec (Vec Bool card) card
entryOf : Grid → Fin card → Fin card → Bool
entryOf V i j = lookup (lookup V i) j
allRows : List (Vec Bool card)
allRows = listVecs allBits card
∈-allRows : (r : Vec Bool card) → r ∈ allRows
∈-allRows r = ∈-listVecs allBits r (λ p → ∈-allBits (lookup r p))
allGrids : List Grid
allGrids = listVecs allRows card
∈-allGrids : (V : Grid) → V ∈ allGrids
∈-allGrids V = ∈-listVecs allRows V (λ i → ∈-allRows (lookup V i))
```
The **grid of a decidable congruence** `d` records the decision of `d` on each pair
of enumerated elements; `entryOf-gridOf`{.AgdaFunction} reads that bit back, by two
applications of `lookup∘tabulate`{.AgdaFunction}.
```agda
gridOf : DecCon 𝑨 (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ) → Grid
gridOf d = tabulate (λ i → tabulate (λ j → does (proj₂ d (enum i) (enum j))))
entryOf-gridOf : ∀ d → (i j : Fin card)
→ entryOf (gridOf d) i j ≡ does (proj₂ d (enum i) (enum j))
entryOf-gridOf d i j =
trans (cong (λ r → lookup r j)
(lookup∘tabulate (λ i → tabulate (λ j → does (proj₂ d (enum i) (enum j)))) i))
(lookup∘tabulate (λ j → does (proj₂ d (enum i) (enum j))) j)
```
Each grid is decoded to a `DecCon`{.AgdaFunction} by generating the congruence of the
enumerated pairs it keeps: `gpairs V`{.AgdaFunction} is the list of those pairs, and
`decode V`{.AgdaFunction} is `Cg-DecCon`{.AgdaFunction} of it. The whole enumeration
`allDecCons`{.AgdaFunction} decodes every grid.
```agda
idxPairs : List (Fin card × Fin card)
idxPairs = cartesianProduct (allFin card) (allFin card)
gpairs : Grid → List (𝕌[ 𝑨 ] × 𝕌[ 𝑨 ])
gpairs V = map (λ p → enum (proj₁ p) , enum (proj₂ p))
(filter (λ p → T? (entryOf V (proj₁ p) (proj₂ p))) idxPairs)
decodeCon : Grid → Con 𝑨 (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ)
decodeCon V = Cg {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (gpairs V))
abstract
decodeDec : (V : Grid) → ∀ x y → Dec (proj₁ (decodeCon V) x y)
decodeDec V = proj₂ (Cg-DecCon 𝑭 𝑺 (gpairs V))
decode : Grid → DecCon 𝑨 (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ)
decode V = decodeCon V , decodeDec V
allDecCons : List (DecCon 𝑨 (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ))
allDecCons = map decode allGrids
```
#### Completeness of the enumeration
For any `DecCon`{.AgdaFunction} `d`, its decoded grid is on the list and is `≑` to `d`.
The `≑` is the L2 reconstruction argument, specialized: soundness
(`fromGrid⊆d`{.AgdaFunction}) reads every kept pair as `d`-related and absorbs the
`≈`-steps with `con-resp-≈`{.AgdaFunction}, so `Cg-least`{.AgdaFunction} contains the
generated congruence in `d` (`gridCg⊆d`{.AgdaFunction}); completeness
(`d⊆gridCg`{.AgdaFunction}) sends a `d`-related pair to its enumerated
representatives, which the grid keeps, so `base`{.AgdaInductiveConstructor} contains
`d` in the generated congruence. Because the underlying congruence
`decodeCon`{.AgdaFunction} is transparent, `proj₁ (decode (gridOf d))` reduces to
`Cg (fromPairs (gpairs (gridOf d)))` and the two containments apply on the nose.
```agda
grid-related : ∀ d → All (λ q → ConRel d (proj₁ q) (proj₂ q)) (gpairs (gridOf d))
grid-related d =
map⁺ {P = λ (q₁ , q₂) → ConRel d q₁ q₂}
{f = λ (p₁ , p₂) → enum p₁ , enum p₂}
(all-map keptRelated
(all-filter (λ (p₁ , p₂) → T? (entryOf (gridOf d) p₁ p₂)) idxPairs))
where
keptRelated : {(p₁ , p₂) : Fin card × Fin card}
→ T (entryOf (gridOf d) p₁ p₂) → ConRel d (enum p₁) (enum p₂)
keptRelated {(p₁ , p₂)} t =
does-out (proj₂ d (enum p₁) (enum p₂)) (subst T (entryOf-gridOf d p₁ p₂) t)
fromGrid⊆d : ∀ d → {x y : 𝕌[ 𝑨 ]}
→ fromPairs {𝑨 = 𝑨} (gpairs (gridOf d)) x y → ConRel d x y
fromGrid⊆d d mem = let (aθb , x≈a , y≈b) = lookupAny (grid-related d) mem
in con-resp-≈ (proj₁ d) x≈a y≈b aθb
gridCg⊆d : ∀ d → {x y : 𝕌[ 𝑨 ]}
→ Gen (fromPairs {𝑨 = 𝑨} (gpairs (gridOf d))) x y → ConRel d x y
gridCg⊆d d = Cg-least (proj₁ d) (fromGrid⊆d d)
d⊆gridCg : ∀ d → {x y : 𝕌[ 𝑨 ]}
→ ConRel d x y → Gen {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (gpairs (gridOf d))) x y
d⊆gridCg d {x} {y} dxy = base (lose grid-keeps (≈sym (idx-≈ x) , ≈sym (idx-≈ y)))
where
eθe : ConRel d (enum (idx x)) (enum (idx y))
eθe = con-resp-≈ (proj₁ d) (idx-≈ x) (idx-≈ y) dxy
kept : T (entryOf (gridOf d) (idx x) (idx y))
kept = subst T (sym (entryOf-gridOf d (idx x) (idx y)))
(does-in (proj₂ d (enum (idx x)) (enum (idx y))) eθe)
grid-keeps : (enum (idx x) , enum (idx y)) ∈ gpairs (gridOf d)
grid-keeps =
∈-map⁺ (λ (p₁ , p₂) → enum p₁ , enum p₂)
(∈-filter⁺ (λ (p₁ , p₂) → T? (entryOf (gridOf d) p₁ p₂))
(∈-cartesianProduct⁺ (∈-allFin (idx x)) (∈-allFin (idx y))) kept)
decode∈list : ∀ d → decode (gridOf d) ∈ allDecCons
decode∈list d = ∈-map⁺ decode (∈-allGrids (gridOf d))
d≑decode : ∀ d → proj₁ d ≑ proj₁ (decode (gridOf d))
d≑decode d = d⊆gridCg d , gridCg⊆d d
allDecCons-complete : ∀ d → Σ[ e ∈ DecCon 𝑨 _ ] (e ∈ allDecCons) × (proj₁ d ≑ proj₁ e)
allDecCons-complete d = decode (gridOf d) , decode∈list d , d≑decode d
```
#### The Layer-D witness
Assembling the enumeration and its completeness gives the constructive
`FiniteCongruencesᵈ`{.AgdaRecord} witness for any finite finitary algebra, with no
classical assumption. This is the L3 deliverable and the constructive counterpart of
`FiniteCongruences`{.AgdaRecord}; the passage to the *semantic* completeness of
`FiniteCongruences`{.AgdaRecord} is the separate classical bridge (L4), not derivable
here.
```agda
open FiniteCongruencesᵈ
FiniteAlgebra→FiniteCongruencesᵈ : {𝑨 : Algebra {𝑆 = 𝑆} α ρ}
→ FiniteAlgebra 𝑨 → FiniteSignature 𝑆 → FiniteCongruencesᵈ 𝑨
FiniteAlgebra→FiniteCongruencesᵈ 𝑭 𝑺 .consᵈ = allDecCons 𝑭 𝑺
FiniteAlgebra→FiniteCongruencesᵈ 𝑭 𝑺 .completeᵈ = allDecCons-complete 𝑭 𝑺
```
--------------------------------------
[^1]: It is the single Layer-S→Layer-D bridge of ADR-008
(`docs/adr/008-two-layer-congruence-discipline.md`).
[^2]: first described as Lemma L3 in the design note
`docs/notes/flrp-two-layer-congruences.md` § 3.
[^3]: `FiniteCongruencesᵈ`{.AgdaRecord} is the working notion the FLRP program
quantifies over, while `FiniteCongruences`{.AgdaRecord} remains the semantic form,
crossed to exactly once through the bridge.
[^4]: As ADR-008 records, the enumeration is exponential and exists to discharge the
completeness *theorem*; in practice the congruence list is supplied by certificates
(WP-6), not by running `allGrids`{.AgdaFunction}.