---
layout: default
title : "Setoid.Congruences module (Agda Universal Algebra Library)"
date : "2021-09-17"
author: "agda-algebras development team"
---

### Congruences

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

A **congruence** of a setoid algebra `𝑨` is an equivalence relation on its carrier
that contains the setoid equality and is compatible with every basic operation.
Congruences are what quotients are taken by, and the lattice they form is one of
the two main invariants of an algebra, the other being its subalgebra structure.

This is a barrel module: it declares nothing of its own and re-exports the
following:

+  [Setoid.Congruences.Basic][]: `IsCongruence`{.AgdaRecord}, the bundled
   `Con`{.AgdaFunction}, the quotient `_╱_`{.AgdaFunction}, and the least and
   greatest congruences;
+  [Setoid.Congruences.Generation][]: the congruence generated by a relation, and
   its universal property;
+  [Setoid.Congruences.Lattice][] and [Setoid.Congruences.CompleteLattice][]: the
   congruence lattice, and its completeness;
+  [Setoid.Congruences.Permutability][] and [Setoid.Congruences.ChainJoin][]:
   permuting congruences and joins computed as chains;
+  [Setoid.Congruences.Monolith][]: monolithic algebras, those with a unique
   minimal nonzero congruence;
+  [Setoid.Congruences.Simple][]: simple algebras, in the implication form that
   concrete instances inhabit;
+  [Setoid.Congruences.Finite][], [Setoid.Congruences.Presented][] and
   [Setoid.Congruences.Certificates][]: the decidable and finitely presented
   cases, and the machine-checked certificates built on them;
+  [Setoid.Congruences.Properties][]: everything else.


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

module Setoid.Congruences where

open import Setoid.Congruences.Basic            public
open import Setoid.Congruences.Certificates     public
open import Setoid.Congruences.ChainJoin        public
open import Setoid.Congruences.CompleteLattice  public
open import Setoid.Congruences.Finite           public
open import Setoid.Congruences.Generation       public
open import Setoid.Congruences.Lattice          public
open import Setoid.Congruences.Monolith         public
open import Setoid.Congruences.Permutability    public
open import Setoid.Congruences.Presented        public
open import Setoid.Congruences.Properties       public
open import Setoid.Congruences.Simple           public
```