---
layout: default
file: "src/Classical/Structures/Lattice/Free/Universal.lagda.md"
title: "Classical.Structures.Lattice.Free.Universal module"
date: "2026-10-07"
author: "the agda-algebras development team"
---
### The free lattice and its universal property
This is the [Classical.Structures.Lattice.Free.Universal][] module of the [Agda Universal Algebra Library][].
The free lattice `FL(X)` on a set `X` is a lattice generated by `X` into which
every map from `X` to a lattice extends, uniquely, to a homomorphism. This module
constructs it from Whitman's order of [Classical.Structures.Lattice.Free.Whitman][]
and proves the universal property, together with the two halves of Whitman's
theorem ([Freese, Ježek, and Nation (1995)][], Theorem 1.11): the rules of
`_≤ʷ_`{.AgdaDatatype} are *sound*, valid in every lattice under every assignment,
and *complete*, deriving every inequality that holds in all lattices.
The construction is order first, as the library builds every lattice whose
operations come from an order. The carrier is the set of lattice terms, its
equality is mutual `_≤ʷ_`{.AgdaDatatype}, and formal meet and join are the
infimum and supremum of `_≤ʷ_`{.AgdaDatatype}; the standard library then derives
the lattice equations, and `setoidEqsToLattice`{.AgdaFunction} packages the result
as a `Lattice`{.AgdaFunction}. Nothing about `FL X`{.AgdaFunction} is quotiented:
its elements are terms, and when equality of generators is decidable, so is its
equality, by `_≈ʷ?_`{.AgdaFunction}.
The proofs of soundness and completeness are short, and their shortness is the
point of the syntactic route. Soundness is an induction on derivations, one line
per rule, each rule valid by the order properties of [Classical.Properties.Lattice][].
Completeness needs no induction on derivations: an inequality valid in every
lattice is valid in `FL X`{.AgdaFunction} under the assignment of each generator
to itself, which evaluates every term to itself.
<!--
```agda
{-# OPTIONS --without-K --exact-split --safe #-}
module Classical.Structures.Lattice.Free.Universal where
open import Agda.Primitive using () renaming ( Set to Type )
open import Data.Fin.Patterns using ( 0F ; 1F )
open import Data.Product using ( _,_ ; proj₁ ; proj₂ )
open import Function using ( Func ; _⇔_ ; mk⇔ )
open import Level using ( Level ; _⊔_ )
open import Relation.Binary using ( Setoid )
open import Relation.Binary.Lattice using ( Supremum ; Infimum )
renaming ( Lattice to OrderLattice
; IsLattice to IsOrderLattice )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl ; cong₂ ; subst₂ )
import Algebra.Lattice.Bundles as AlgLatticeBundles
import Algebra.Lattice.Properties.Lattice as AlgLatticeProperties
import Relation.Binary.Lattice.Properties.Lattice as OrderLatticeProperties
open import Classical.Operations using ( pair )
open import Classical.Properties.Lattice using ( module Lattice-Order )
open import Classical.Signatures.Lattice using ( ∧-Op ; ∨-Op )
open import Classical.Structures.Interpret using ( interp-cong )
open import Classical.Structures.Lattice.Basic using ( Lattice ; setoidEqsToLattice )
open import Classical.Structures.Lattice.Free.Term using ( LatTerm ; ℊ ; _∧̇_ ; _∨̇_
; module Evaluation )
open import Classical.Structures.Lattice.Free.Whitman
using ( _≤ʷ_ ; _≈ʷ_ ; ≈ʷ-isEquivalence ; ∨≤ ; ℊ≤∧ ; ∧≤∧ ; ℊ≤ℊ ; ℊ≤∨ˡ ; ℊ≤∨ʳ
; ∧ˡ≤ℊ ; ∧ʳ≤ℊ ; ∧ˡ≤∨ ; ∧ʳ≤∨ ; ∧≤∨ˡ ; ∧≤∨ʳ ; ℊ≤ℊ-inv ; ≤∧ ; ≤ʷ-refl ; ≤ʷ-trans
; ∨̇-upperˡ ; ∨̇-upperʳ ; ∧̇-lowerˡ ; ∧̇-lowerʳ )
open import Setoid.Algebras.Basic using ( 𝔻[_] ; 𝕌[_] )
open import Setoid.Homomorphisms.Basic using ( hom ; mkhom ; compatible-map
; IsHom )
open Func renaming ( to to _⟨$⟩_ )
private variable
α ρ χ : Level
X : Type χ
x y : X
s t : LatTerm X
```
-->
#### The carrier
The carrier setoid of `FL X`{.AgdaFunction} is the set of lattice terms under mutual
`_≤ʷ_`{.AgdaDatatype}.
```agda
FL-setoid : (X : Type χ) → Setoid χ χ
FL-setoid X = record { Carrier = LatTerm X
; _≈_ = _≈ʷ_
; isEquivalence = ≈ʷ-isEquivalence
}
```
#### The order-theoretic lattice
Formal join is the supremum of `_≤ʷ_`{.AgdaDatatype} (`FL-supremum`{.AgdaFunction}):
the two upper-bound clauses are `∨̇-upperˡ`{.AgdaFunction} and
`∨̇-upperʳ`{.AgdaFunction}, and the least-upper-bound clause is rule 2,
`∨≤`{.AgdaInductiveConstructor}. Formal meet is the infimum
(`FL-infimum`{.AgdaFunction}), with `≤∧`{.AgdaFunction} as the greatest-lower-bound
clause. With reflexivity, transitivity, and antisymmetry (which holds by the
definition of `_≈ʷ_`{.AgdaFunction}), these make the standard library's
order-theoretic lattice `FL-OrderLattice X`{.AgdaFunction}.
```agda
FL-supremum : Supremum (_≤ʷ_ {X = X}) _∨̇_
FL-supremum s t = ∨̇-upperˡ , ∨̇-upperʳ , λ u → ∨≤
FL-infimum : Infimum (_≤ʷ_ {X = X}) _∧̇_
FL-infimum s t = ∧̇-lowerˡ , ∧̇-lowerʳ , λ u → ≤∧
FL-isOrderLattice : IsOrderLattice (_≈ʷ_ {X = X}) _≤ʷ_ _∨̇_ _∧̇_
FL-isOrderLattice = record
{ isPartialOrder = record
{ isPreorder = record
{ isEquivalence = ≈ʷ-isEquivalence
; reflexive = proj₁
; trans = ≤ʷ-trans
}
; antisym = _,_
}
; supremum = FL-supremum
; infimum = FL-infimum
}
FL-OrderLattice : (X : Type χ) → OrderLattice χ χ χ
FL-OrderLattice X = record
{ Carrier = LatTerm X
; _≈_ = _≈ʷ_
; _≤_ = _≤ʷ_
; _∨_ = _∨̇_
; _∧_ = _∧̇_
; isLattice = FL-isOrderLattice
}
```
#### The free lattice
`FL X`{.AgdaFunction} is the equational lattice the library works with. The eight
equations of `Th-Lattice`{.AgdaFunction} come from the order: the standard
library's `algLattice`{.AgdaFunction} turns `FL-OrderLattice X`{.AgdaFunction} into
an algebraic lattice with commutativity, associativity, congruence, and
absorption, its `Properties` module supplies idempotence, and the second
absorption law, in the shape `(a ∧ b) ∨ a ≈ a` that `Th-Lattice`{.AgdaFunction}
states, is read off the order directly. The interpretation clauses of
`setoidEqsToLattice`{.AgdaFunction} apply the argument tuple, so the curried meet
and join of `FL X`{.AgdaFunction} are definitionally `_∧̇_`{.AgdaInductiveConstructor}
and `_∨̇_`{.AgdaInductiveConstructor}.
```agda
FL : (X : Type χ) → Lattice χ χ
FL X = setoidEqsToLattice (FL-setoid X) _∧̇_ _∨̇_
(λ {x} {y} {u} {v} → AL.∧-cong {x} {y} {u} {v})
(λ {x} {y} {u} {v} → AL.∨-cong {x} {y} {u} {v})
(λ {a} {b} {c} → AL.∧-assoc a b c)
(λ {a} {b} → AL.∧-comm a b)
(λ {a} → AP.∧-idem a)
(λ {a} {b} {c} → AL.∨-assoc a b c)
(λ {a} {b} → AL.∨-comm a b)
(λ {a} → AP.∨-idem a)
(λ {a} {b} → AL.∧-absorbs-∨ a b)
(∨≤ ∧̇-lowerˡ ≤ʷ-refl , ∨̇-upperʳ)
where
module OP = OrderLatticeProperties (FL-OrderLattice X)
module AL = AlgLatticeBundles.Lattice OP.algLattice
module AP = AlgLatticeProperties OP.algLattice
```
#### The order of the free lattice is Whitman's order
`Lattice-Order`{.AgdaModule} of [Classical.Properties.Lattice][] equips every
lattice with its meet order, `a ≤ b` meaning `a ∧ b ≈ a`. In
`FL X`{.AgdaFunction} that order is `_≤ʷ_`{.AgdaDatatype}: one direction is the
infimum property, the other transitivity through the lower bound
`∧̇-lowerʳ`{.AgdaFunction}. The generators are pairwise distinct in
`FL X`{.AgdaFunction}, since two generators are related by rule 1 alone
(`ℊ-injective`{.AgdaFunction}); this is the part of [Freese, Ježek, and Nation
(1995)][], Corollary 1.5, that says `x ≤ y` implies `x = y` for generators.
```agda
module _ {X : Type χ} where
open Lattice-Order (FL X) using ( _≤_ )
≤ʷ→≤ : s ≤ʷ t → s ≤ t
≤ʷ→≤ p = ∧̇-lowerˡ , ≤∧ ≤ʷ-refl p
≤→≤ʷ : s ≤ t → s ≤ʷ t
≤→≤ʷ (_ , s≤s∧t) = ≤ʷ-trans s≤s∧t ∧̇-lowerʳ
ℊ-injective : ℊ x ≈ʷ ℊ y → x ≡ y
ℊ-injective (p , _) = ℊ≤ℊ-inv p
```
#### Every term evaluates to itself
The *generic assignment* sends each generator `x` to the term `ℊ x`. Evaluating a
term in `FL X`{.AgdaFunction} under it rebuilds the term, constructor for
constructor, so every element of `FL X`{.AgdaFunction} is the value of a term in
the generators (`⟦⟧-ℊ`{.AgdaFunction}), and `FL X`{.AgdaFunction} is generated by
`X`. The equality is propositional, by induction, because the meet and join of
`FL X`{.AgdaFunction} are the formal ones.
```agda
module _ {X : Type χ} where
open Evaluation (FL X) using ( ⟦_⟧ )
⟦⟧-ℊ : (t : LatTerm X) → ⟦ t ⟧ ℊ ≡ t
⟦⟧-ℊ (ℊ x) = refl
⟦⟧-ℊ (s ∧̇ t) = cong₂ _∧̇_ (⟦⟧-ℊ s) (⟦⟧-ℊ t)
⟦⟧-ℊ (s ∨̇ t) = cong₂ _∨̇_ (⟦⟧-ℊ s) (⟦⟧-ℊ t)
```
#### Validity
`𝑳 ⊧ s ≤ t`{.AgdaFunction} says that the inequality `s ≤ t` holds in the lattice
`𝑳`{.AgdaBound} under every assignment of its elements to the generators, for the
meet order of `Lattice-Order`{.AgdaModule}. It is the inequational counterpart of
the satisfaction relation `_⊧_≈_`{.AgdaFunction} of
[Setoid.Varieties.EquationalLogic][], stated for lattice terms.
```agda
infix 4 _⊧_≤_
_⊧_≤_ : {X : Type χ} → Lattice α ρ → LatTerm X → LatTerm X → Type (χ ⊔ α ⊔ ρ)
_⊧_≤_ {X = X} 𝑳 s t = (η : X → 𝕌[ proj₁ 𝑳 ]) → ⟦ s ⟧ η ≤ ⟦ t ⟧ η
where
open Evaluation 𝑳 using ( ⟦_⟧ )
open Lattice-Order 𝑳 using ( _≤_ )
```
#### Soundness
Every rule of `_≤ʷ_`{.AgdaDatatype} is valid in every lattice, so every derivation
is (`≤ʷ-sound`{.AgdaFunction}). The proof is an induction on the derivation with
one clause per constructor: rule 2 is `∨-least`{.AgdaFunction}, rule 3 is
`∧-greatest`{.AgdaFunction}, rule 1 is reflexivity, and each disjunct of rules 4,
5, and 6 composes the inductive hypothesis with a bound of
`Lattice-Order`{.AgdaModule} (`∨-upperˡ`{.AgdaFunction} and
`∨-upperʳ`{.AgdaFunction} below a join, `∧-lowerˡ`{.AgdaFunction} and
`∧-lowerʳ`{.AgdaFunction} above a meet). Antisymmetry turns soundness for
`_≤ʷ_`{.AgdaDatatype} into soundness for `_≈ʷ_`{.AgdaFunction}
(`≈ʷ-sound`{.AgdaFunction}): terms that are equal in `FL X`{.AgdaFunction} have
equal values in every lattice.
```agda
module _ (𝑳 : Lattice α ρ) where
open Evaluation 𝑳 using ( ⟦_⟧ )
open Lattice-Order 𝑳 using ( ≤-refl ; ≤-trans ; ≤-antisym ; ∧-lowerˡ ; ∧-lowerʳ
; ∧-greatest ; ∨-upperˡ ; ∨-upperʳ ; ∨-least )
open Setoid 𝔻[ proj₁ 𝑳 ] using ( _≈_ )
≤ʷ-sound : s ≤ʷ t → 𝑳 ⊧ s ≤ t
≤ʷ-sound (∨≤ p q) η = ∨-least (≤ʷ-sound p η) (≤ʷ-sound q η)
≤ʷ-sound (ℊ≤∧ p q) η = ∧-greatest (≤ʷ-sound p η) (≤ʷ-sound q η)
≤ʷ-sound (∧≤∧ p q) η = ∧-greatest (≤ʷ-sound p η) (≤ʷ-sound q η)
≤ʷ-sound (ℊ≤ℊ refl) η = ≤-refl
≤ʷ-sound (ℊ≤∨ˡ p) η = ≤-trans (≤ʷ-sound p η) ∨-upperˡ
≤ʷ-sound (ℊ≤∨ʳ p) η = ≤-trans (≤ʷ-sound p η) ∨-upperʳ
≤ʷ-sound (∧ˡ≤ℊ p) η = ≤-trans ∧-lowerˡ (≤ʷ-sound p η)
≤ʷ-sound (∧ʳ≤ℊ p) η = ≤-trans ∧-lowerʳ (≤ʷ-sound p η)
≤ʷ-sound (∧ˡ≤∨ p) η = ≤-trans ∧-lowerˡ (≤ʷ-sound p η)
≤ʷ-sound (∧ʳ≤∨ p) η = ≤-trans ∧-lowerʳ (≤ʷ-sound p η)
≤ʷ-sound (∧≤∨ˡ p) η = ≤-trans (≤ʷ-sound p η) ∨-upperˡ
≤ʷ-sound (∧≤∨ʳ p) η = ≤-trans (≤ʷ-sound p η) ∨-upperʳ
≈ʷ-sound : s ≈ʷ t → (η : X → 𝕌[ proj₁ 𝑳 ]) → ⟦ s ⟧ η ≈ ⟦ t ⟧ η
≈ʷ-sound (p , q) η = ≤-antisym (≤ʷ-sound p η) (≤ʷ-sound q η)
```
#### Completeness
Conversely, an inequality that holds in every lattice is derivable
(`≤ʷ-complete`{.AgdaFunction}). It holds in particular in `FL X`{.AgdaFunction}
under the generic assignment, where it reads `s ≤ t` for the meet order of
`FL X`{.AgdaFunction}, because each side evaluates to itself; and that order is
`_≤ʷ_`{.AgdaDatatype}. The hypothesis is needed only for lattices at the level
of `X`, where `FL X`{.AgdaFunction} lives; together with soundness, which holds
at every level, it is Whitman's theorem (`≤ʷ⇔⊧`{.AgdaFunction}).
```agda
≤ʷ-complete : {X : Type χ} {s t : LatTerm X} → ((𝑳 : Lattice χ χ) → 𝑳 ⊧ s ≤ t) → s ≤ʷ t
≤ʷ-complete {X = X} {s} {t} valid =
subst₂ _≤ʷ_ (⟦⟧-ℊ s) (⟦⟧-ℊ t) (≤→≤ʷ (valid (FL X) ℊ))
≤ʷ⇔⊧ : {X : Type χ} {s t : LatTerm X} → s ≤ʷ t ⇔ ((𝑳 : Lattice χ χ) → 𝑳 ⊧ s ≤ t)
≤ʷ⇔⊧ = mk⇔ (λ p 𝑳 → ≤ʷ-sound 𝑳 p) ≤ʷ-complete
```
#### The universal property
Fix a lattice `𝑳`{.AgdaBound} and a map `f`{.AgdaBound} from the generators to its
carrier. Evaluation under `f`{.AgdaBound} is a setoid map out of
`FL X`{.AgdaFunction} (`FL-extend`{.AgdaFunction}), well defined because equal
terms have equal values (`≈ʷ-sound`{.AgdaFunction}). It is a homomorphism
(`FL-extend-hom`{.AgdaFunction}), since it sends each formal operation to the
operation of `𝑳`{.AgdaBound}, and it extends `f`{.AgdaBound}, definitionally
(`FL-extend-ℊ`{.AgdaFunction}). It is the only such homomorphism
(`FL-extend-unique`{.AgdaFunction}): a homomorphism that agrees with
`f`{.AgdaBound} on the generators agrees with `FL-extend`{.AgdaFunction} on
every term, by induction on the term. So `FL X`{.AgdaFunction} is freely
generated by `X`.
```agda
module _ {X : Type χ} (𝑳 : Lattice α ρ) (f : X → 𝕌[ proj₁ 𝑳 ]) where
open Evaluation 𝑳 using ( ⟦_⟧ )
open Setoid 𝔻[ proj₁ 𝑳 ] using ( _≈_ ) renaming ( refl to ≈refl ; trans to ≈trans )
FL-extend : Func 𝔻[ proj₁ (FL X) ] 𝔻[ proj₁ 𝑳 ]
FL-extend = record { to = λ t → ⟦ t ⟧ f ; cong = λ s≈t → ≈ʷ-sound 𝑳 s≈t f }
FL-extend-compatible : compatible-map (proj₁ (FL X)) (proj₁ 𝑳) FL-extend
FL-extend-compatible {∧-Op} = interp-cong (proj₁ 𝑳) ∧-Op λ { 0F → ≈refl ; 1F → ≈refl }
FL-extend-compatible {∨-Op} = interp-cong (proj₁ 𝑳) ∨-Op λ { 0F → ≈refl ; 1F → ≈refl }
FL-extend-hom : hom (proj₁ (FL X)) (proj₁ 𝑳)
FL-extend-hom = mkhom (proj₁ (FL X)) (proj₁ 𝑳) FL-extend FL-extend-compatible
FL-extend-ℊ : (x : X) → FL-extend ⟨$⟩ ℊ x ≈ f x
FL-extend-ℊ x = ≈refl
```
The uniqueness proof unfolds `h ⟨$⟩ (s ∧̇ t)` as `h` applied to the meet of
`FL X`{.AgdaFunction} at the argument tuple `pair s t`, moves `h` inside by its
compatibility with `∧-Op`, and closes with the inductive hypotheses at the two
argument positions (`args`); a join is the same with `∨-Op`.
```agda
FL-extend-unique : (h : hom (proj₁ (FL X)) (proj₁ 𝑳))
→ (∀ x → proj₁ h ⟨$⟩ ℊ x ≈ f x) → (t : LatTerm X) → proj₁ h ⟨$⟩ t ≈ ⟦ t ⟧ f
FL-extend-unique h hℊ (ℊ x) = hℊ x
FL-extend-unique h hℊ (s ∧̇ t) =
≈trans (IsHom.compatible (proj₂ h) {∧-Op} {pair s t}) (interp-cong (proj₁ 𝑳) ∧-Op args)
where
args : ∀ i → proj₁ h ⟨$⟩ pair s t i ≈ pair (⟦ s ⟧ f) (⟦ t ⟧ f) i
args 0F = FL-extend-unique h hℊ s
args 1F = FL-extend-unique h hℊ t
FL-extend-unique h hℊ (s ∨̇ t) =
≈trans (IsHom.compatible (proj₂ h) {∨-Op} {pair s t}) (interp-cong (proj₁ 𝑳) ∨-Op args)
where
args : ∀ i → proj₁ h ⟨$⟩ pair s t i ≈ pair (⟦ s ⟧ f) (⟦ t ⟧ f) i
args 0F = FL-extend-unique h hℊ s
args 1F = FL-extend-unique h hℊ t
```