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

### Finitely presented congruences

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

A congruence is **finitely presented** when it is the congruence generated by a
finite list of pairs.  A presentation is the first thing a decision procedure
needs, but it is not by itself enough: deciding membership in the generated
congruence also requires the carrier and the signature to be finite, supplied as
`FiniteAlgebra`{.AgdaRecord} of [Setoid.Algebras.Finite][] and
`FiniteSignature`{.AgdaRecord} of [Setoid.Signatures.Finite][].  Given all three,
equality in the quotient is decidable, which is what the certificate machinery of
[Setoid.Congruences.Certificates][] runs on.

This is a barrel module, re-exporting [Setoid.Congruences.Presented.Basic][] for
the presentation itself and [Setoid.Congruences.Presented.Decidable][] for the
decision procedure.

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

module Setoid.Congruences.Presented where

open import Setoid.Congruences.Presented.Basic      public
open import Setoid.Congruences.Presented.Decidable  public
```