---
layout: default
file: "src/Setoid/Congruences/Permutability.lagda.md"
title: "Setoid.Congruences.Permutability module"
date: "2026-06-19"
author: "the agda-algebras development team"
---

### Relation composition and congruence permutability

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

[Setoid.Congruences.Lattice][] and [Setoid.Congruences.Generation][] built the
*congruence lattice* of an algebra — meet (intersection), join (generated by the
union), and the containment order.  Permutability is a property *transverse* to that
lattice: it asks how two congruences sit relative to one another under
**relation composition**, an operation that is not part of the lattice structure and
does not in general return a congruence.

The relational composition `θ ∘ φ` holds at `(x , y)` exactly when some `z` has
`x θ z` and `z φ y`.  Two congruences **permute** when `θ ∘ φ ⊆ φ ∘ θ`; because the
reverse inclusion is the same statement with `θ` and `φ` swapped, the assertion that
*every* pair of congruences permute is the assertion that composition is commutative
on `Con 𝑨`.
An algebra (or a variety) with this property is called **congruence-permutable**, and
this is the property that the classical *Maltsev condition* characterizes by a single
ternary term ([Setoid.Varieties.Maltsev][]).

This module is pure congruence theory: it depends only on the congruence record of
[Setoid.Congruences.Basic][], not on terms, interpretations, or the lattice bundles.

<!--
```agda
{-# OPTIONS --cubical-compatible --exact-split --safe #-}

open import Overture using ( 𝓞 ; 𝓥 ; Signature )

module Setoid.Congruences.Permutability {𝑆 : Signature 𝓞 𝓥} where

-- Imports from Agda and the Agda Standard Library ----------------------------
open import Agda.Primitive   using () renaming ( Set to Type )
open import Data.Product     using ( _×_ ; _,_ ; ∃-syntax ; proj₁ )
open import Level            using ( Level ; _⊔_ )
open import Relation.Binary  using ( Setoid ; IsEquivalence )
                             renaming ( Rel to BinaryRel ; _⇒_ to _⊆_ )

-- Imports from the Agda Universal Algebra Library ----------------------------
open import Setoid.Algebras.Basic     {𝑆 = 𝑆}  using ( ov ; Algebra ; 𝕌[_] )
open import Setoid.Congruences.Basic  {𝑆 = 𝑆}  using ( Con ; is-equivalence )

private variable α ρ ℓ : Level
```
-->

#### Relation composition of congruences

For congruences `θ φ : Con 𝑨 ℓ` we write `θ ∘ φ` for the composition of their
underlying relations: `(θ ∘ φ) x y` is inhabited by a witness `z` together with
proofs `x θ z` and `z φ y`.  The composition is a *bare* binary relation, not a
congruence — it need not be transitive — so its codomain is `BinaryRel`, and the
existential bumps the relation level from `ℓ` to `α ⊔ ℓ` (the witness ranges over
the carrier `𝕌[ 𝑨 ] : Type α`).

```agda
module _ {𝑨 : Algebra α ρ} where
  _∘_ : Con 𝑨 ℓ → Con 𝑨 ℓ → BinaryRel 𝕌[ 𝑨 ] (α ⊔ ℓ)
  ((_θ_ , _) ∘ (_φ_ , _)) x y = ∃[ z ] x θ z × z φ y
  infixr  _∘_
```

A composition `θ ∘ φ` always *contains* each factor, because a congruence is
reflexive (it contains the underlying setoid equality, hence is reflexive in the
ordinary sense).  Inserting the relevant reflexive step on the right (resp. left)
embeds `θ` (resp. `φ`) into the composite.

```agda
  open IsEquivalence using (refl)

  -- θ ⊆ θ ∘ φ
  ∘-inˡ : (θ φ : Con 𝑨 ℓ){x y : 𝕌[ 𝑨 ]} → proj₁ θ x y → (θ ∘ φ) x y
  ∘-inˡ _ (_ , isCongφ) {x}{y} xθy = y , xθy , isCongφ .is-equivalence .refl

  -- φ ⊆ θ ∘ φ
  ∘-inʳ : (θ φ : Con 𝑨 ℓ){x y : 𝕌[ 𝑨 ]} → proj₁ φ x y → (θ ∘ φ) x y
  ∘-inʳ (_ , isCongθ) _ {x} xφy = x , isCongθ .is-equivalence .refl , xφy
```

#### Permutability

A pair of congruences **permutes** when `θ ∘ φ` is contained in `φ ∘ θ`.
(Here `_⊆_` is the standard-library relation-inclusion `_⇒_`: `R ⊆ S` means
`∀ {x y} → R x y → S x y`.)

```agda
  -- θ and φ permute: θ ∘ φ ⊆ φ ∘ θ.
  Permutes : Con 𝑨 ℓ → Con 𝑨 ℓ → Type (α ⊔ ℓ)
  Permutes θ φ = θ ∘ φ ⊆ φ ∘ θ
```

#### Congruence-permutable algebras

An algebra is **congruence-permutable** (at relation level `ℓ`) when *every* pair of
its congruences permutes.

```agda
CongruencePermutable : (𝑨 : Algebra α ρ)(ℓ : Level) → Type (α ⊔ ρ ⊔ ov ℓ)
CongruencePermutable 𝑨 ℓ = (θ φ : Con 𝑨 ℓ) → Permutes θ φ
```

Permutability of every pair is symmetric "for free"; from `Permutes θ φ` and
`Permutes φ θ` we get mutual containment: `θ ∘ φ ⊆ φ ∘ θ` and `φ ∘ θ ⊆ θ ∘ φ`.
Hence in a congruence-permutable algebra composition is genuinely commutative on
congruences — the conventional statement `θ ∘ φ = φ ∘ θ`, read here as mutual
containment, the setoid notion of equal relations.

```agda
module _ {𝑨 : Algebra α ρ} where

  -- In a congruence-permutable algebra, every two congruences commute (both
  -- inclusions hold), since CP supplies `Permutes` in either order.
  permutable⇒commute : CongruencePermutable 𝑨 ℓ
    → (θ φ : Con 𝑨 ℓ) → (θ ∘ φ) ⊆ (φ ∘ θ) × (φ ∘ θ) ⊆ (θ ∘ φ)
  permutable⇒commute cp θ φ = cp θ φ , cp φ θ
```