Setoid.Congruences.Finite¶

Finitely enumerable congruence lattices¶

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

Setoid.Congruences.Finite.Basic supplies the finiteness interface for congruences, that is, decidable congruences (DecCon) and the record type FiniteCongruences.

Setoid.Congruences.Finite.Decidable supplies the constructive counterpart: a finite list of DecCons that is complete — every decidable congruence is ≑ to a listed one — with no classical axiom.

{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Setoid.Congruences.Finite where

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