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.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.

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