---
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.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 --cubical-compatible --exact-split --safe #-}

module Setoid.Congruences where

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