---
layout: default
file: "src/Classical/Signatures/Finite.lagda.md"
title: "Classical.Signatures.Finite module"
date: "2026-07-12"
author: "the agda-algebras development team"
---
### Finite finitary witnesses for concrete signatures
This is the [Classical.Signatures.Finite][] module of the [Agda Universal Algebra Library][].
The record `FiniteSignature`{.AgdaRecord} of [Setoid.Signatures.Finite][] packages
what it means for a signature to be *finite finitary*: a finite surjective
enumeration of its operation symbols, plus the `Finitary`{.AgdaFunction} witness
that every arity is finite. This module supplies the following canonical
sanity-check instances:[^1]
+ `Sig-Lattice`{.AgdaFunction} ([Classical.Signatures.Lattice][]): two binary
operation symbols; both halves of the witness are finite case splits;
+ `Sig-Group`{.AgdaFunction} ([Classical.Signatures.Group][]): three operation
symbols, of arities two, zero, and one;
+ `Sig-Unary A`{.AgdaFunction} ([Classical.Signatures.Unary][]): one unary symbol
per element of `A`; the witness is exactly an enumeration of `A`.
#### A caveat on enumerations up to `≈`
The symbol type of a signature is a bare type, so `opEnum-sur`{.AgdaField} demands
surjectivity up to propositional equality `_≡_`. The carrier enumeration of a
`FiniteAlgebra`{.AgdaRecord} ([Setoid.Algebras.Finite][]) is surjective only up to
the carrier's setoid equality `_≈_`, which is *not* enough here. Indeed, on a
quotient carrier the enumeration hits every element up to the coarser `≈` while
missing raw elements up to `≡`.
Consequently `Sig-Unary-FiniteSignature`{.AgdaFunction} below asks for an honest
`_≡_`-surjective enumeration of the bare type `A` rather than for a
`FiniteAlgebra`{.AgdaRecord} witness. In the intended applications this costs
nothing; in points of fact,
+ for a concrete finite group the raw carrier is typically `Fin n` or a finite
data type, where `≈` *is* `≡`;
+ the raw carrier of a quotient `G / H` is that of `G` itself, so the same bare
enumeration serves all coset algebras of `G` with no choice of coset
representatives.
<!--
```agda
{-# OPTIONS --without-K --exact-split --safe #-}
module Classical.Signatures.Finite where
open import Agda.Primitive using () renaming ( Set to Type )
open import Data.Fin.Base using ( Fin ; zero ; suc )
open import Data.Nat.Base using ( ℕ )
open import Data.Product using ( _,_ ; ∃-syntax )
open import Function.Construct.Identity using ( ↔-id )
open import Level using ( Level )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl )
open import Classical.Signatures.Group using ( Sig-Group ; ∙-Op ; ε-Op ; ⁻¹-Op )
open import Classical.Signatures.Lattice using ( Sig-Lattice ; ∧-Op ; ∨-Op )
open import Classical.Signatures.Unary using ( Sig-Unary )
open import Setoid.Congruences.ChainJoin using ( Finitary )
open import Setoid.Signatures.Finite using ( FiniteSignature )
open FiniteSignature
```
-->
#### The lattice signature is finite and finitary
Both lattice operation symbols are binary, so the `Finitary`{.AgdaFunction}
witness names the identity bijection once per symbol, and the symbol enumeration
lists the two symbols.
```agda
Sig-Lattice-Finitary : Finitary Sig-Lattice
Sig-Lattice-Finitary ∧-Op = 2 , ↔-id _
Sig-Lattice-Finitary ∨-Op = 2 , ↔-id _
Sig-Lattice-FiniteSignature : FiniteSignature Sig-Lattice
Sig-Lattice-FiniteSignature .opCard = 2
Sig-Lattice-FiniteSignature .opEnum zero = ∧-Op
Sig-Lattice-FiniteSignature .opEnum (suc zero) = ∨-Op
Sig-Lattice-FiniteSignature .opEnum-sur ∧-Op = zero , refl
Sig-Lattice-FiniteSignature .opEnum-sur ∨-Op = suc zero , refl
Sig-Lattice-FiniteSignature .finitary = Sig-Lattice-Finitary
```
#### The group signature is finite and finitary
The three group operation symbols have arities `Fin 2`, `Fin 0`, and `Fin 1`, each
already of the shape `Finitary`{.AgdaFunction} demands, so the arity half is again
the identity bijection in each case. From this witness we can derive the
decidable generated congruence of [Setoid.Congruences.Presented.Decidable][], and
hence the normal closure of [Classical.Structures.Group.NormalClosure][], over a
finite group.
```agda
Sig-Group-Finitary : Finitary Sig-Group
Sig-Group-Finitary ∙-Op = 2 , ↔-id _
Sig-Group-Finitary ε-Op = 0 , ↔-id _
Sig-Group-Finitary ⁻¹-Op = 1 , ↔-id _
Sig-Group-FiniteSignature : FiniteSignature Sig-Group
Sig-Group-FiniteSignature .opCard = 3
Sig-Group-FiniteSignature .opEnum zero = ∙-Op
Sig-Group-FiniteSignature .opEnum (suc zero) = ε-Op
Sig-Group-FiniteSignature .opEnum (suc (suc zero)) = ⁻¹-Op
Sig-Group-FiniteSignature .opEnum-sur ∙-Op = zero , refl
Sig-Group-FiniteSignature .opEnum-sur ε-Op = suc zero , refl
Sig-Group-FiniteSignature .opEnum-sur ⁻¹-Op = suc (suc zero) , refl
Sig-Group-FiniteSignature .finitary = Sig-Group-Finitary
```
#### The unary signature over an enumerated symbol type
Given a surjective (up to `_≡_`) enumeration of the bare type `A`, the unary
signature over `A` is finite and finitary: the symbol enumeration is the given one,
and every arity is `Fin 1` definitionally.
```agda
module _ {ℓ : Level}{A : Type ℓ}
(n : ℕ)(e : Fin n → A)(e-sur : (a : A) → ∃[ i ] e i ≡ a) where
Sig-Unary-FiniteSignature : FiniteSignature (Sig-Unary A)
Sig-Unary-FiniteSignature .opCard = n
Sig-Unary-FiniteSignature .opEnum = e
Sig-Unary-FiniteSignature .opEnum-sur = e-sur
Sig-Unary-FiniteSignature .finitary _ = 1 , ↔-id _
```
--------------------------------------
[^1]: We place these instances here, rather than beside the record, because concrete
signatures live in the `Classical/` tree and the `Setoid/` tree does not import it.