Setoid.Congruences.Presented

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 of Setoid.Algebras.Finite and FiniteSignature 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.

{-# OPTIONS --without-K --exact-split --safe #-}

module Setoid.Congruences.Presented where

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