Setoid.Congruences.Certificates.Lattice

The whole-lattice certificate checker

This is the Setoid.Congruences.Certificates.Lattice module of the Agda Universal Algebra Library.

A whole-lattice certificate (LatticeCert of Setoid.Congruences.Certificates.Schema) claims the entire congruence lattice of a finite finitary algebra: a list of congruences as normal-form parent vectors, a principal-congruence pointer for every carrier index pair, and meet and join tables.

This module checks those claims — reusing the per-congruence machinery of Setoid.Congruences.Certificates.Congruence wholesale — and delivers the Layer-D payoff: a FiniteCongruencesᵈ instance (Setoid.Congruences.Finite.Decidable) whose congruence list is the certificate's, with constructive completeness and no Cg-dec anywhere.

The checked conditions (LatticeCertOK, one decidable bundle):

• each listed vector is in Freese normal form, coherent, and edge-compatible — so each is a congruence that is ≑ to what its own forest edges generate, with no trace (table≑CgEdges);
• distinct positions carry distinct vectors (injOK) — by the root determination lemma below, normal form upgrades this to "≑-distinct congruences", which pins every pointer uniquely;
• the bot entry relates only ≈-equal elements — so it is ≑ the congruence generated by the empty pair list;
• each principal pointer's entry contains its pair and carries a valid Freese trace covering its partition — obligations C1–C3 for the seed list (i , j) ∷ [];
• each join entry contains both arguments' forest edges and carries a valid trace covering its partition — C1–C3 for the concatenated edge seed list, whence the entry is ≑ the join ∨ of its arguments;
• each meet entry's blocks are exactly the pointwise intersections of its arguments' blocks — meets of partitions are definitional, so no trace.

Constructive completeness. For an arbitrary decidable congruence d, the reconstruction argument of Setoid.Congruences.Presented.Basic (re-run on the index-pair list relatedIdx d, exactly as Setoid.Congruences.Finite.Decidable re-runs it on grid pairs) gives

proj₁ d ≑ Cg (fromPairs (carrierPairs (relatedIdx d)))

and a fold of the certificate's prin and join tables over that pair list (foldIdx) lands on a listed entry provably ≑ to the same generated congruence, one Cg-of-cons step at a time (Cg-++-∨).

The fold executes only d's own decision procedure and table lookups — never a closure computation — so completeᵈ is both constructive and cheap.

The module also exports the order-theoretic consequences the FLRP layer needs (FLRP.Certificates): entryInj (≑ forces equal positions), ⊆→meetIdem / meetIdem→⊆ (containment of entries is meet-table idempotence), indexOf with d≑fold / fold-entry / fold-mono (the completeness fold as a monotone retraction onto the list) — everything an order isomorphism with a target lattice's meet order will consume.

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

module Setoid.Congruences.Certificates.Lattice where

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

-- Imports from the Agda Standard Library -----------------------------------
open import Data.Fin.Base         using  ( Fin ; _≤_ )
open import Data.Fin.Properties   using  ( all? ; ≤-antisym )
                                  renaming ( _≟_ to _≟ᶠ_ )
open import Data.List.Base        using  ( List ; [] ; _∷_ ; map ; _++_
                                         ; filter ; allFin ; cartesianProduct )
open import Data.List.Membership.Propositional
                                  using  ( _∈_ ; lose ; find )
open import Data.List.Membership.Propositional.Properties
                                  using  ( ∈-map⁺ ; ∈-map⁻ ; ∈-filter⁺
                                         ; ∈-filter⁻ ; ∈-allFin
                                         ; ∈-cartesianProduct⁺ )
open import Data.List.Properties  using  ( map-++ )
open import Data.List.Relation.Unary.All
                                  using  ( All ; [] ; _∷_ )
open import Data.List.Relation.Unary.All.Properties
                                  using  ( all-filter )
open import Data.List.Relation.Unary.Any
                                  using  ( here ; there )
open import Data.List.Relation.Unary.Any.Properties
                                  using  ( ++⁺ˡ ; ++⁺ʳ ; ++⁻ )
open import Data.Nat.Base         using  ( ℕ )
open import Data.Product          using  ( _×_ ; _,_ ; proj₁ ; proj₂ )
open import Data.Sum.Base         using  ( inj₁ ; inj₂ )
open import Level                 using  ( Level ; _⊔_ ; lift ; lower )
open import Relation.Binary       using  ( Setoid )
open import Relation.Binary.PropositionalEquality
                                  using  ( _≡_ ; sym ; trans ; subst )
open import Relation.Nullary.Decidable
                                  using  ( Dec ; map′ ; _×-dec_ ; _→-dec_ )

-- Imports from the Agda Universal Algebra Library ----------------------------
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.Finite.Decidable         using  ( FiniteCongruencesᵈ )
open import Setoid.Congruences.Generation               using  ( Gen ; Cg ; base ; rfl
                                                               ; Cg-least ; _∨_
                                                               ; ∨-least )
open import Setoid.Congruences.Lattice                  using  ( _⊆_ ; _≑_
                                                               ; ≑-sym ; ≑-trans )
open import Setoid.Congruences.Presented                using  ( fromPairs
                                                               ; con-resp-≈ )
open import Setoid.Congruences.Certificates.Schema      using  ( parent
                                                               ; NormalForm
                                                               ; normalForm?
                                                               ; forestEdges
                                                               ; LatticeCert )
open import Setoid.Congruences.Certificates.Congruence  using  ( module CertCheck )
open import Setoid.Signatures.Finite                    using  ( FiniteSignature )

private variable α ρ : Level

The ambient algebra and certificate

Fix the finite finitary algebra, open the per-congruence checker CertCheck 𝑭 𝑺, and fix a whole-lattice certificate lc of any list length m.

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

  open CertCheck 𝑭 𝑺
  open FiniteAlgebra 𝑭 using ( _≟_ ; card ; enum ; enum-sur )
  open FiniteSignature 𝑺 using ( opCard )
  open Setoid 𝔻[ 𝑨 ] using ( _≈_ )
    renaming ( sym to ≈sym ; trans to ≈trans )

  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)

The checked conditions

LatticeCertOK bundles every checked condition of one whole-lattice certificate; latticeCertOK? decides the whole bundle at once, so a concrete emitted certificate is discharged by a single from-yes. Each field is a bounded sweep built from the deciders of Setoid.Congruences.Certificates.Congruence and Schema.

  module _ {m : ℕ} (lc : LatticeCert card opCard arOf m) where
    open LatticeCert lc

    -- The seed list of a claimed join: both arguments' forest edges.
    joinSeeds : Fin m → Fin m → List IdxPair
    joinSeeds k l = forestEdges (partAt k) ++ forestEdges (partAt l)

    record LatticeCertOK : Type ρ where
      constructor mkLatticeCertOK
      field
        -- every listed vector is in Freese normal form, coherent, and
        -- edge-compatible
        nfOK    : ∀ k → NormalForm (partAt k)
        cohOK   : ∀ k → Coherent (partAt k)
        ecOK    : ∀ k → EdgeCompat (partAt k)
        -- distinct positions carry distinct vectors
        injOK   : ∀ k l → (∀ i → parent (partAt k) i ≡ parent (partAt l) i)
                        → k ≡ l
        -- the bot entry relates only ≈-equal elements
        botOK   : ∀ i j → SameBlock (partAt bot) i j → enum i ≈ enum j
        -- principal pointers: pair containment, trace validity, coverage
        prinRespOK  : ∀ i j → Respects (partAt (prin i j)) ((i , j) ∷ [])
        prinTrOK    : ∀ i j → TraceValid ((i , j) ∷ []) (prinTrace i j)
        prinCovOK   : ∀ i j → Covers (partAt (prin i j))
                                     (replayRoots (merges (prinTrace i j)))
        -- join entries: edge containment, trace validity, coverage
        joinRespOK  : ∀ k l → Respects (partAt (join k l)) (joinSeeds k l)
        joinTrOK    : ∀ k l → TraceValid (joinSeeds k l) (joinTrace k l)
        joinCovOK   : ∀ k l → Covers (partAt (join k l))
                                     (replayRoots (merges (joinTrace k l)))
        -- meet entries: blocks are exactly the pointwise intersections
        meetOKˡ  : ∀ k l i j → SameBlock (partAt (meet k l)) i j
                             → SameBlock (partAt k) i j
        meetOKʳ  : ∀ k l i j → SameBlock (partAt (meet k l)) i j
                             → SameBlock (partAt l) i j
        meetOK²  : ∀ k l i j → SameBlock (partAt k) i j
                             → SameBlock (partAt l) i j
                             → SameBlock (partAt (meet k l)) i j

    -- One decision for the whole bundle.
    latticeCertOK? : Dec LatticeCertOK
    latticeCertOK? = map′
      (λ (nf , coh , ec , inj , bot′ , pr , pt , pc , jr , jt , jc , m₁ , m₂ , m₃)
         → mkLatticeCertOK nf coh ec inj bot′ pr pt pc jr jt jc m₁ m₂ m₃)
      (λ ok → let open LatticeCertOK ok in
         nfOK , cohOK , ecOK , injOK , botOK , prinRespOK , prinTrOK , prinCovOK
              , joinRespOK , joinTrOK , joinCovOK , meetOKˡ , meetOKʳ , meetOK²)
      (     all? (λ k → normalForm? (partAt k))
      ×-dec all? (λ k → coherent? (partAt k))
      ×-dec all? (λ k → edgeCompat? (partAt k))
      ×-dec all? (λ k → all? (λ l →
              all? (λ i → parent (partAt k) i ≟ᶠ parent (partAt l) i)
                →-dec (k ≟ᶠ l)))
      ×-dec all? (λ i → all? (λ j →
              (parent (partAt bot) i ≟ᶠ parent (partAt bot) j)
                →-dec (enum i ≟ enum j)))
      ×-dec all? (λ i → all? (λ j → respects? (partAt (prin i j)) ((i , j) ∷ [])))
      ×-dec all? (λ i → all? (λ j → traceValid? ((i , j) ∷ []) (prinTrace i j)))
      ×-dec all? (λ i → all? (λ j → covers? (partAt (prin i j))
                                      (replayRoots (merges (prinTrace i j)))))
      ×-dec all? (λ k → all? (λ l → respects? (partAt (join k l)) (joinSeeds k l)))
      ×-dec all? (λ k → all? (λ l → traceValid? (joinSeeds k l) (joinTrace k l)))
      ×-dec all? (λ k → all? (λ l → covers? (partAt (join k l))
                                      (replayRoots (merges (joinTrace k l)))))
      ×-dec all? (λ k → all? (λ l → all? (λ i → all? (λ j →
              (parent (partAt (meet k l)) i ≟ᶠ parent (partAt (meet k l)) j)
                →-dec (parent (partAt k) i ≟ᶠ parent (partAt k) j)))))
      ×-dec all? (λ k → all? (λ l → all? (λ i → all? (λ j →
              (parent (partAt (meet k l)) i ≟ᶠ parent (partAt (meet k l)) j)
                →-dec (parent (partAt l) i ≟ᶠ parent (partAt l) j)))))
      ×-dec all? (λ k → all? (λ l → all? (λ i → all? (λ j →
              (parent (partAt k) i ≟ᶠ parent (partAt k) j)
                →-dec ((parent (partAt l) i ≟ᶠ parent (partAt l) j)
                →-dec (parent (partAt (meet k l)) i ≟ᶠ parent (partAt (meet k l)) j)))))))

The certified entries

From here on assume the certificate checked. Every listed entry is a (decidable) congruence, ≑ to what its own forest edges generate.

    module _ (OK : LatticeCertOK) where
      open LatticeCertOK OK

      -- The congruence at a list position, and its decidable packaging.
      entryCon : Fin m → Con 𝑨 (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ)
      entryCon k = tableCon (partAt k) (cohOK k) (ecOK k)

      entryDec : Fin m → DecCon 𝑨 (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ)
      entryDec k = tableDecCon (partAt k) (cohOK k) (ecOK k)

      -- Every entry is ≑ the congruence generated by its own forest edges.
      entry≑Edges : ∀ k →
        entryCon k ≑ Cg {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs (forestEdges (partAt k))))
      entry≑Edges k =
        table≑CgEdges (partAt k) (cohOK k) (ecOK k) (proj₁ (nfOK k))

Root determination. Two ≑-equal entries have pointwise-equal parent vectors, because in normal form the root of an index is the least member of its block, and ≑ makes the blocks coincide. With injOK this upgrades to injectivity of the entry list, the fact that pins every table pointer.

      -- Containment of entries transports same-block facts.
      sameBlock-mono : ∀ k l → entryCon k ⊆ entryCon l
        →  ∀ i j → SameBlock (partAt k) i j → SameBlock (partAt l) i j
      sameBlock-mono k l sub i j sb =
        trans (sym (bridge l i))
              (trans (lower (sub (lift (trans (bridge k i)
                                              (trans sb (sym (bridge k j)))))))
                     (bridge l j))
        where
        -- the chosen index of an enumerated element is same-block with it
        bridge : ∀ k′ i′ → parent (partAt k′) (idx (enum i′)) ≡ parent (partAt k′) i′
        bridge k′ i′ = cohOK k′ (idx (enum i′)) i′ (idx-≈ (enum i′))

      -- ≑-equal entries have pointwise-equal (normal-form) parent vectors.
      rootsAgree : ∀ k l → entryCon k ≑ entryCon l
        →  ∀ i → parent (partAt k) i ≡ parent (partAt l) i
      rootsAgree k l (k⊆l , l⊆k) i = ≤-antisym pk≤pl pl≤pk
        where
        -- i is same-block with its k-root, so also in l; then l-decreasingness
        -- at the k-root bounds the l-root, and symmetrically.
        sb-l : SameBlock (partAt l) i (parent (partAt k) i)
        sb-l = sameBlock-mono k l k⊆l i (parent (partAt k) i)
                              (sym (proj₁ (nfOK k) i))

        pl≤pk : parent (partAt l) i ≤ parent (partAt k) i
        pl≤pk = subst (_≤ parent (partAt k) i) (sym sb-l)
                      (proj₂ (nfOK l) (parent (partAt k) i))

        sb-k : SameBlock (partAt k) i (parent (partAt l) i)
        sb-k = sameBlock-mono l k l⊆k i (parent (partAt l) i)
                              (sym (proj₁ (nfOK l) i))

        pk≤pl : parent (partAt k) i ≤ parent (partAt l) i
        pk≤pl = subst (_≤ parent (partAt l) i) (sym sb-k)
                      (proj₂ (nfOK k) (parent (partAt l) i))

      -- The entry list is ≑-injective.
      entryInj : ∀ k l → entryCon k ≑ entryCon l → k ≡ l
      entryInj k l eq = injOK k l (rootsAgree k l eq)

The verified tables

The bot entry generates nothing; the principal entries generate their pair; the join entries are the joins; the meet entries are the intersections.

      -- The bot entry is ≑ the congruence generated by no pairs.
      bot≑CgEmpty : entryCon bot ≑ Cg {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs []))
      bot≑CgEmpty = below , above
        where
        below : entryCon bot ⊆ Cg {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs []))
        below (lift sb) =
          rfl (≈trans (≈sym (idx-≈ _)) (≈trans (botOK _ _ sb) (idx-≈ _)))

        above : Cg {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs [])) ⊆ entryCon bot
        above = Cg-least (entryCon bot) (λ ())

      -- Each principal entry is ≑ the congruence generated by its pair.
      prin≑ : ∀ i j →
        entryCon (prin i j) ≑ Cg {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs ((i , j) ∷ [])))
      prin≑ i j =
        table≑Cg (partAt (prin i j)) ((i , j) ∷ []) (prinTrace i j)
                 (cohOK (prin i j)) (ecOK (prin i j))
                 (prinRespOK i j) (prinTrOK i j) (prinCovOK i j)

      -- Each join entry is ≑ the congruence generated by both edge lists.
      join≑Seeds : ∀ k l →
        entryCon (join k l) ≑ Cg {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs (joinSeeds k l)))
      join≑Seeds k l =
        table≑Cg (partAt (join k l)) (joinSeeds k l) (joinTrace k l)
                 (cohOK (join k l)) (ecOK (join k l))
                 (joinRespOK k l) (joinTrOK k l) (joinCovOK k l)

Generation splits along list concatenation: Cg of an appended pair list is the join of the two generated congruences. (Instantiated at a singleton head this is the cons step the completeness fold consumes, since ((i , j) ∷ []) ++ ps is (i , j) ∷ ps.)

      -- Cg distributes over ++ as a join.
      Cg-++-∨ : (ps qs : List IdxPair)
        →  Cg {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs (ps ++ qs)))
             ≑ (Cg {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs ps))
                 ∨ Cg {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs qs)))
      Cg-++-∨ ps qs = below , above
        where
        CgL CgR Cg++ : Con 𝑨 (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ)
        CgL   = Cg {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs ps))
        CgR   = Cg {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs qs))
        Cg++  = Cg {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs (ps ++ qs)))

        -- carrierPairs distributes over ++
        cp-++ : carrierPairs (ps ++ qs) ≡ carrierPairs ps ++ carrierPairs qs
        cp-++ = map-++ (λ p → enum (proj₁ p) , enum (proj₂ p)) ps qs

        below : Cg++ ⊆ (CgL ∨ CgR)
        below = Cg-least (CgL ∨ CgR) split
          where
          split : ∀ {x y} → fromPairs {𝑨 = 𝑨} (carrierPairs (ps ++ qs)) x y
            →    proj₁ (CgL ∨ CgR) x y
          split {x} {y} mem
            with ++⁻ (carrierPairs ps)
                     (subst (λ zs → fromPairs {𝑨 = 𝑨} zs x y) cp-++ mem)
          ... | inj₁ inl = base (inj₁ (base inl))
          ... | inj₂ inr = base (inj₂ (base inr))

        above : (CgL ∨ CgR) ⊆ Cg++
        above = ∨-least CgL CgR Cg++
          (Cg-least Cg++ (λ {x} {y} inl → base
            (subst (λ zs → fromPairs {𝑨 = 𝑨} zs x y) (sym cp-++) (++⁺ˡ inl))))
          (Cg-least Cg++ (λ {x} {y} inr → base
            (subst (λ zs → fromPairs {𝑨 = 𝑨} zs x y) (sym cp-++)
                   (++⁺ʳ (carrierPairs ps) inr))))

      -- ∨ is a congruence for ≑.
      ∨-cong-≑ : {θ θ′ φ φ′ : Con 𝑨 (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ)}
        →  θ ≑ θ′ → φ ≑ φ′ → (θ ∨ φ) ≑ (θ′ ∨ φ′)
      ∨-cong-≑ {θ} {θ′} {φ} {φ′} (t , t′) (f , f′) =
        ∨-least θ  φ  (θ′ ∨ φ′) (λ p → base (inj₁ (t p)))  (λ p → base (inj₂ (f p))) ,
        ∨-least θ′ φ′ (θ ∨ φ)   (λ p → base (inj₁ (t′ p))) (λ p → base (inj₂ (f′ p)))

      -- A verified join entry is the join of its argument entries.
      join≑∨ : ∀ k l → entryCon (join k l) ≑ (entryCon k ∨ entryCon l)
      join≑∨ k l =
        ≑-trans {θ = entryCon (join k l)} {φ = CgJS} {ψ = entryCon k ∨ entryCon l}
          (join≑Seeds k l)
          (≑-trans {θ = CgJS} {φ = CgE k ∨ CgE l} {ψ = entryCon k ∨ entryCon l}
            (Cg-++-∨ (forestEdges (partAt k)) (forestEdges (partAt l)))
            (≑-sym {θ = entryCon k ∨ entryCon l} {φ = CgE k ∨ CgE l}
              (∨-cong-≑ {θ = entryCon k} {θ′ = CgE k}
                        {φ = entryCon l} {φ′ = CgE l}
                        (entry≑Edges k) (entry≑Edges l))))
        where
        CgE : Fin m → Con 𝑨 (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ)
        CgE k′ = Cg {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs (forestEdges (partAt k′))))

        CgJS : Con 𝑨 (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ)
        CgJS = Cg {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs (joinSeeds k l)))

The meet entries, read at the carrier level. Because the table relation is same-block at the chosen indices, the checked sweeps apply directly, with no coherence bridges.

      -- The meet entry is below both arguments ...
      meet-⊆ˡ : ∀ k l → entryCon (meet k l) ⊆ entryCon k
      meet-⊆ˡ k l (lift sb) = lift (meetOKˡ k l _ _ sb)

      meet-⊆ʳ : ∀ k l → entryCon (meet k l) ⊆ entryCon l
      meet-⊆ʳ k l (lift sb) = lift (meetOKʳ k l _ _ sb)

      -- ... and above anything below both.
      meet-⊇ : ∀ k l {x y} → proj₁ (entryCon k) x y → proj₁ (entryCon l) x y
        →  proj₁ (entryCon (meet k l)) x y
      meet-⊇ k l (lift sbk) (lift sbl) = lift (meetOK² k l _ _ sbk sbl)

      -- Containment of entries is idempotence of the meet table, both ways.
      meetIdem→⊆ : ∀ k l → meet k l ≡ k → entryCon k ⊆ entryCon l
      meetIdem→⊆ k l e {x} {y} relk =
        meet-⊆ʳ k l (subst (λ z → proj₁ (entryCon z) x y) (sym e) relk)

      ⊆→meetIdem : ∀ k l → entryCon k ⊆ entryCon l → meet k l ≡ k
      ⊆→meetIdem k l sub = entryInj (meet k l) k
        ( (λ p → meet-⊆ˡ k l p) , (λ p → meet-⊇ k l p (sub p)) )

Reconstruction on the related index pairs

For an arbitrary decidable congruence d, the index pairs it relates reconstruct it: proj₁ d ≑ Cg (fromPairs (carrierPairs (relatedIdx d))). This re-runs the two-containment argument of Setoid.Congruences.Presented.Basic on the index-pair list — the same choice, for the same filter/map-fusion reason, as in Setoid.Congruences.Finite.Decidable.

      -- All index pairs, and those a decidable congruence relates.
      idxPairsAll : List IdxPair
      idxPairsAll = cartesianProduct (allFin card) (allFin card)

      relatedIdx : DecCon 𝑨 (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ) → List IdxPair
      relatedIdx d =
        filter (λ p → proj₂ d (enum (proj₁ p)) (enum (proj₂ p))) idxPairsAll

      -- Soundness: every kept pair is d-related.
      relatedIdx-sound : ∀ d →
        All (λ p → ConRel d (enum (proj₁ p)) (enum (proj₂ p))) (relatedIdx d)
      relatedIdx-sound d =
        all-filter (λ p → proj₂ d (enum (proj₁ p)) (enum (proj₂ p))) idxPairsAll

      -- Hence the presented relation of the kept pairs is contained in d:
      -- walk any list of d-related pairs to the presenting one and absorb
      -- the ≈-steps.
      private
        fromAll⊆d : (d : DecCon 𝑨 (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ)) (qs : List IdxPair)
          →  All (λ p → ConRel d (enum (proj₁ p)) (enum (proj₂ p))) qs
          →  ∀ {x y} → fromPairs {𝑨 = 𝑨} (carrierPairs qs) x y → ConRel d x y
        fromAll⊆d d []        []            ()
        fromAll⊆d d (q ∷ qs)  (rel ∷ _)     (here (x≈ , y≈)) =
          con-resp-≈ (proj₁ d) x≈ y≈ rel
        fromAll⊆d d (q ∷ qs)  (_ ∷ rall)    (there mem) = fromAll⊆d d qs rall mem

      fromRelated⊆d : ∀ d {x y}
        →  fromPairs {𝑨 = 𝑨} (carrierPairs (relatedIdx d)) x y → ConRel d x y
      fromRelated⊆d d = fromAll⊆d d (relatedIdx d) (relatedIdx-sound d)

      -- ... and conversely d is contained in what they generate.
      d⊆CgRelated : ∀ d {x y} → ConRel d x y
        →  Gen {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs (relatedIdx d))) x y
      d⊆CgRelated d {x} {y} dxy =
        base (lose kept (≈sym (idx-≈ x) , ≈sym (idx-≈ y)))
        where
        -- d relates the enumerated representatives, so their pair is kept
        eθe : ConRel d (enum (idx x)) (enum (idx y))
        eθe = con-resp-≈ (proj₁ d) (idx-≈ x) (idx-≈ y) dxy

        kept : (enum (idx x) , enum (idx y)) ∈ carrierPairs (relatedIdx d)
        kept = ∈-map⁺ (λ p → enum (proj₁ p) , enum (proj₂ p))
                 (∈-filter⁺ (λ p → proj₂ d (enum (proj₁ p)) (enum (proj₂ p)))
                   (∈-cartesianProduct⁺ (∈-allFin (idx x)) (∈-allFin (idx y)))
                   eθe)

      -- Reconstruction along the related index pairs.
      d≑CgRelated : ∀ d →
        proj₁ d ≑ Cg {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs (relatedIdx d)))
      d≑CgRelated d = d⊆CgRelated d , Cg-least (proj₁ d) (fromRelated⊆d d)

The completeness fold

Fold the principal and join tables over a pair list. Each step is one table lookup, and the result is provably ≑ the congruence the list generates.

      -- The certificate's entry for a pair list: fold prin through join.
      foldIdx : List IdxPair → Fin m
      foldIdx []        = bot
      foldIdx (p ∷ ps)  = join (prin (proj₁ p) (proj₂ p)) (foldIdx ps)

      -- The fold lands on the generated congruence.
      fold-≑ : (ps : List IdxPair)
        →  entryCon (foldIdx ps) ≑ Cg {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs ps))
      fold-≑ [] = bot≑CgEmpty
      fold-≑ ((i , j) ∷ ps) =
        ≑-trans {θ = entryCon (foldIdx ((i , j) ∷ ps))}
                {φ = entryCon (prin i j) ∨ entryCon (foldIdx ps)}
                {ψ = CgAll}
          (join≑∨ (prin i j) (foldIdx ps))
          (≑-trans {θ = entryCon (prin i j) ∨ entryCon (foldIdx ps)}
                   {φ = Cg₁ ∨ CgPs} {ψ = CgAll}
            (∨-cong-≑ {θ = entryCon (prin i j)} {θ′ = Cg₁}
                      {φ = entryCon (foldIdx ps)} {φ′ = CgPs}
                      (prin≑ i j) (fold-≑ ps))
            (≑-sym {θ = CgAll} {φ = Cg₁ ∨ CgPs} (Cg-++-∨ ((i , j) ∷ []) ps)))
        where
        Cg₁ CgPs CgAll : Con 𝑨 (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ)
        Cg₁    = Cg {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs ((i , j) ∷ [])))
        CgPs   = Cg {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs ps))
        CgAll  = Cg {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs ((i , j) ∷ ps)))

      -- The certificate's representative of an arbitrary decidable congruence.
      indexOf : DecCon 𝑨 (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ) → Fin m
      indexOf d = foldIdx (relatedIdx d)

      -- d is ≑ its representative entry.
      d≑fold : ∀ d → proj₁ d ≑ proj₁ (entryDec (indexOf d))
      d≑fold d =
        ≑-trans {θ = proj₁ d}
                {φ = Cg {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs (relatedIdx d)))}
                {ψ = entryCon (indexOf d)}
          (d≑CgRelated d)
          (≑-sym {θ = entryCon (indexOf d)}
                 {φ = Cg {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs (relatedIdx d)))}
                 (fold-≑ (relatedIdx d)))

      -- The fold retracts the entry list onto itself.
      fold-entry : ∀ k → indexOf (entryDec k) ≡ k
      fold-entry k =
        entryInj (indexOf (entryDec k)) k
          (≑-sym {θ = entryCon k} {φ = entryCon (indexOf (entryDec k))}
                 (d≑fold (entryDec k)))

Monotonicity of the fold: a containment of decidable congruences transfers to their kept-pair lists, hence — through Cg-monotonicity and the fold's ≑-characterizations, composed inline — to their representative entries.

      -- Containment transfers to the kept pairs' presented relations.
      relatedIdx-mono : (d e : DecCon 𝑨 (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ))
        →  (∀ {x y} → ConRel d x y → ConRel e x y)
        →  ∀ {x y} → fromPairs {𝑨 = 𝑨} (carrierPairs (relatedIdx d)) x y
        →  fromPairs {𝑨 = 𝑨} (carrierPairs (relatedIdx e)) x y
      relatedIdx-mono d e sub {x} {y} mem with find mem
      ... | (q , q∈cp , pay)
        with ∈-map⁻ (λ p → enum (proj₁ p) , enum (proj₂ p)) q∈cp
      ...   | (p , p∈flt , q≡fp)
        with ∈-filter⁻ (λ p′ → proj₂ d (enum (proj₁ p′)) (enum (proj₂ p′)))
                       {xs = idxPairsAll} p∈flt
      ...     | (p∈all , dRel) =
        lose (∈-map⁺ (λ p′ → enum (proj₁ p′) , enum (proj₂ p′))
               (∈-filter⁺ (λ p′ → proj₂ e (enum (proj₁ p′)) (enum (proj₂ p′)))
                 p∈all (sub dRel)))
             (subst (λ q′ → (x ≈ proj₁ q′) × (y ≈ proj₂ q′)) q≡fp pay)

      -- The fold is monotone.
      fold-mono : (d e : DecCon 𝑨 (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ))
        →  (∀ {x y} → ConRel d x y → ConRel e x y)
        →  entryCon (indexOf d) ⊆ entryCon (indexOf e)
      fold-mono d e sub p =
        proj₂ (fold-≑ (relatedIdx e))
          (Cg-least (Cg {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (carrierPairs (relatedIdx e))))
                    (λ r → base (relatedIdx-mono d e sub r))
                    (proj₁ (fold-≑ (relatedIdx d)) p))

The Layer-D payoff

The certificate's entries, with the fold as completeness witness, form a FiniteCongruencesᵈ instance: a finite list of decidable congruences exhausting the decidable congruences of 𝑨 up to ≑ — supplied by certificate, exactly as ADR-008 anticipated, rather than by the exponential enumeration of Setoid.Congruences.Finite.Decidable.

      open FiniteCongruencesᵈ

      certFiniteCongruencesᵈ : FiniteCongruencesᵈ 𝑨
      certFiniteCongruencesᵈ .consᵈ = map entryDec (allFin m)
      certFiniteCongruencesᵈ .completeᵈ d =
        entryDec (indexOf d)
          , ∈-map⁺ entryDec (∈-allFin (indexOf d))
          , d≑fold d

---