Skip to content

Examples.Setoid.FinitarySignatures

Finiteness witnesses are one-liners

This is the Examples.Setoid.FinitarySignatures module of the Agda Universal Algebra Library.

The finitary Jónsson theorem jonsson-finitary⇒CongruenceDistributiveVariety (Setoid.Varieties.Maltsev.Distributivity) asks for a witness Finitary 𝑆 (Setoid.Congruences.ChainJoin) that every operation symbol of 𝑆 has a finite arity. This module shows that supplying that witness is never a hoop: for the finitary signatures of ordinary universal algebra it is the identity bijection ↔-id, written once (per the signature's shape).

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

module Examples.Setoid.FinitarySignatures where

open import Agda.Primitive                  using () renaming ( Set to Type )
open import Data.Fin.Base                   using ( Fin )
open import Data.Nat.Base                   using ( ℕ )
open import Data.Product                    using ( _,_ )
open import Function.Construct.Identity     using ( ↔-id )
open import Level                           using ( Level )

open import Setoid.Congruences.ChainJoin    using ( Finitary )
open import Setoid.Varieties.Maltsev        using ( Sig-Maltsev ; m-Op )

When a signature's arity function has the shape λ f → Fin (ar f) — the natural way to write a finitary signature — every arity reduces to a concrete Fin, so the finiteness witness is literally λ f → _ , ↔-id _: no case split, no proof obligation.

module _ {𝓞 : Level}{Op : Type 𝓞}(ar : Op → ℕ) where

  finitary-Fin-arity : Finitary (Op , (λ f → Fin (ar f)))
  finitary-Fin-arity f = ar f , ↔-id _

Pattern-matched arities

The signatures already in the library (Sig-Maltsev, and the Classical/ structures) define their arity function by pattern matching on the operation symbol — e.g. ar-Maltsev m-Op = Fin 3. There the witness names the identity bijection once per symbol, still a trivial one-liner.

finitary-Sig-Maltsev : Finitary Sig-Maltsev
finitary-Sig-Maltsev m-Op = _ , ↔-id _

So for any finitary algebra, jonsson-finitary⇒CongruenceDistributiveVariety fin jt applies with fin one of the witnesses above and jt the algebra's Jónsson terms — the finiteness side condition is discharged, never threaded by hand.