Setoid.Congruences

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, the bundled Con, the quotient _╱_, 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.

{-# 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