---
layout: default
file: "src/Examples/Classical/Lattices/L7.lagda.md"
title: "Examples.Classical.Lattices.L7 module"
date: "2026-05-31"
author: "the agda-algebras development team"
---
### Worked example — the seven-element lattice `L7` {#examples-classical-lattices-l7}
This is the [Examples.Classical.Lattices.L7][] module of the [Agda Universal Algebra Library][].
`L7` is a seven-element lattice of interest in the **Finite Lattice Representation
Problem** (FLRP): it is, to our knowledge, the smallest lattice for which no
representation as the congruence lattice of a finite algebra is known. (This is a
question of the FLRP and must not be conflated with the separate
algebraic-complexity / CSP line of work — see `CLAUDE.md`.)
Its shape is as follows. Six of its elements form a `2 × 3` grid — the product of a
two-chain and a three-chain — with bottom `⊥ = (0,0)`, top `⊤ = (1,2)`, two atoms
`(0,1)` and `(1,0)`, and two coatoms `(0,2)` and `(1,1)`. The seventh element `x`
sits beside the grid with `⊥ < x < ⊤` and is incomparable to every nontrivial grid
element; consequently `x` is the *unique* element that is both an atom and a coatom.
Because `x` together with the chain `(1,0) < (1,1)` forms a pentagon `N5`, `L7` is
**not distributive**, so it is a genuine `Lattice` example rather than a
`DistributiveLattice` one.
We label the carrier `Fin 7` by `⊥ = 0`, `(1,0) = 1`, `(0,1) = 2`, `x = 3`,
`(1,1) = 4`, `(0,2) = 5`, `⊤ = 6`, giving the Hasse diagram
```text
⊤ = 6
/ | \
(0,2)=5 (1,1)=4 \
| / \ \
| / \ \
(0,1)=2 (1,0)=1 x = 3
\ / |
\ / |
⊥ = 0 ───────────┘
```
As in the [Heyting chain][Examples.Classical.Lattices.L3Heyting] and the
[finite-group examples][Examples.Classical.Groups.CyclicGroup3], meet and join are given by
Cayley tables and every law is discharged by *decision* over the finite carrier — a
wrong table entry would make some decision compute to `no` and break compilation.
<!--
```agda
{-# OPTIONS --cubical-compatible --exact-split --safe #-}
module Examples.Classical.Lattices.L7 where
open import Data.Fin using ( Fin )
open import Data.Fin.Patterns using ( 0F ; 1F ; 2F ; 3F ; 4F ; 5F ; 6F )
open import Data.Fin.Properties using ( _≟_ ; all? )
open import Data.Vec.Base using ( _∷_ ; [] )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; _≢_ ; refl )
open import Relation.Nullary.Decidable.Core using ( _→-dec_ )
open import Overture.Cayley using ( Table ; ⟦_⟧ ; from-yes )
open import Overture.Operations.Properties using ( Associative? ; Commutative? ; Idempotent?
; Absorbsˡ? ; Absorbsʳ? )
open import Classical.Bundles.Lattice using ( ⟨_⟩ˡᵃ ; ⟪_⟫ˡᵃ )
open import Classical.Properties.Lattice using ( module FiniteOrder )
open import Classical.Small.Structures.Lattice using ( Lattice ; eqsToLattice )
import Classical.Structures.Lattice as Polymorphic
```
-->
#### The Cayley tables {#tables}
The pattern `6F` (`= suc 5F`, from `Data.Fin.Patterns`) is the top element. Meet is
the greatest lower bound, join the least upper bound, read off the diagram above.
| `∧` | 0 | 1 | 2 | 3 | 4 | 5 | 6 | | `∨` | 0 | 1 | 2 | 3 | 4 | 5 | 6 |
|-----|---|---|---|---|---|---|---|---|-----|---|---|---|---|---|---|---|
| 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | | 0 | 0 | 1 | 2 | 3 | 4 | 5 | 6 |
| 1 | 0 | 1 | 0 | 0 | 1 | 0 | 1 | | 1 | 1 | 1 | 4 | 6 | 4 | 6 | 6 |
| 2 | 0 | 0 | 2 | 0 | 2 | 2 | 2 | | 2 | 2 | 4 | 2 | 6 | 4 | 5 | 6 |
| 3 | 0 | 0 | 0 | 3 | 0 | 0 | 3 | | 3 | 3 | 6 | 6 | 3 | 6 | 6 | 6 |
| 4 | 0 | 1 | 2 | 0 | 4 | 2 | 4 | | 4 | 4 | 4 | 4 | 6 | 4 | 6 | 6 |
| 5 | 0 | 0 | 2 | 0 | 2 | 5 | 5 | | 5 | 5 | 6 | 5 | 6 | 6 | 5 | 6 |
| 6 | 0 | 1 | 2 | 3 | 4 | 5 | 6 | | 6 | 6 | 6 | 6 | 6 | 6 | 6 | 6 |
```agda
∧-table : Table 7
∧-table = (0F ∷ 0F ∷ 0F ∷ 0F ∷ 0F ∷ 0F ∷ 0F ∷ [])
∷ (0F ∷ 1F ∷ 0F ∷ 0F ∷ 1F ∷ 0F ∷ 1F ∷ [])
∷ (0F ∷ 0F ∷ 2F ∷ 0F ∷ 2F ∷ 2F ∷ 2F ∷ [])
∷ (0F ∷ 0F ∷ 0F ∷ 3F ∷ 0F ∷ 0F ∷ 3F ∷ [])
∷ (0F ∷ 1F ∷ 2F ∷ 0F ∷ 4F ∷ 2F ∷ 4F ∷ [])
∷ (0F ∷ 0F ∷ 2F ∷ 0F ∷ 2F ∷ 5F ∷ 5F ∷ [])
∷ (0F ∷ 1F ∷ 2F ∷ 3F ∷ 4F ∷ 5F ∷ 6F ∷ [])
∷ []
∨-table : Table 7
∨-table = (0F ∷ 1F ∷ 2F ∷ 3F ∷ 4F ∷ 5F ∷ 6F ∷ [])
∷ (1F ∷ 1F ∷ 4F ∷ 6F ∷ 4F ∷ 6F ∷ 6F ∷ [])
∷ (2F ∷ 4F ∷ 2F ∷ 6F ∷ 4F ∷ 5F ∷ 6F ∷ [])
∷ (3F ∷ 6F ∷ 6F ∷ 3F ∷ 6F ∷ 6F ∷ 6F ∷ [])
∷ (4F ∷ 4F ∷ 4F ∷ 6F ∷ 4F ∷ 6F ∷ 6F ∷ [])
∷ (5F ∷ 6F ∷ 5F ∷ 6F ∷ 6F ∷ 5F ∷ 6F ∷ [])
∷ (6F ∷ 6F ∷ 6F ∷ 6F ∷ 6F ∷ 6F ∷ 6F ∷ [])
∷ []
infixr 7 _∧_
infixr 6 _∨_
_∧_ _∨_ : Fin 7 → Fin 7 → Fin 7
_∧_ = ⟦ ∧-table ⟧
_∨_ = ⟦ ∨-table ⟧
```
#### `L7` as a lattice {#l7-lattice}
The decidable law-checkers all come from `Overture.Operations.Properties`:
associativity, commutativity, and idempotency of each operation, plus the two
absorption laws (`Absorbsˡ?`, `Absorbsʳ?`).
```agda
L7-lattice : Lattice
L7-lattice = eqsToLattice (Fin 7) _∧_ _∨_
(from-yes (Associative? _∧_)) (from-yes (Commutative? _∧_)) (from-yes (Idempotent? _∧_))
(from-yes (Associative? _∨_)) (from-yes (Commutative? _∨_)) (from-yes (Idempotent? _∨_))
(from-yes (Absorbsˡ? _∧_ _∨_)) (from-yes (Absorbsʳ? _∧_ _∨_))
```
#### `L7` is not distributive {#not-distributive}
The pentagon `N5` on `{⊥, (1,0), (1,1), x, ⊤}` witnesses the failure of
distributivity: `(1,0) < (1,1)`, while `x` is incomparable to both and joins each to
`⊤` and meets each to `⊥`. All five facts hold by `refl`.
```agda
n5-chain-l7 : (1F ∧ 4F) ≡ 1F
n5-chain-l7 = refl
n5-x∨lo-l7 : (3F ∨ 1F) ≡ 6F
n5-x∨lo-l7 = refl
n5-x∨hi-l7 : (3F ∨ 4F) ≡ 6F
n5-x∨hi-l7 = refl
n5-x∧lo-l7 : (3F ∧ 1F) ≡ 0F
n5-x∧lo-l7 = refl
n5-x∧hi-l7 : (3F ∧ 4F) ≡ 0F
n5-x∧hi-l7 = refl
L7-not-distributive-l7 : (4F ∧ (1F ∨ 3F)) ≢ ((4F ∧ 1F) ∨ (4F ∧ 3F))
L7-not-distributive-l7 ()
```
#### `x` is the unique atom-coatom {#atom-coatom}
With the meet order `a ≤ b := a ∧ b ≡ a`, an *atom* is a non-bottom element with
nothing strictly below it, and dually for a *coatom*. The order, the `atom`/`coatom`
predicates, and their deciders come from `Classical.Properties.Lattice.FiniteOrder`
(instantiated at `_∧_`, with bottom `0` and top `6`). The atoms of `L7` are
`{(1,0), (0,1), x}` and the coatoms are `{x, (1,1), (0,2)}`, so `x` is the unique
element that is both; this is decided over the finite carrier.
```agda
open FiniteOrder _∧_
open Bounded 0F 6F
x-atom-l7 : atom 3F
x-atom-l7 = from-yes (atom? 3F)
x-coatom-l7 : coatom 3F
x-coatom-l7 = from-yes (coatom? 3F)
unique-atom-coatom-l7 : ∀ a → atom a → coatom a → a ≡ 3F
unique-atom-coatom-l7 = from-yes (all? (λ a → (atom? a) →-dec ((coatom? a) →-dec (a ≟ 3F))))
```
#### Acceptance checks {#acceptance}
The `Lattice-Op` accessors interpret to the tabulated meet and join on the nose, and
the bundle bridge round-trips; both discharged by `refl`.
```agda
open Polymorphic.Lattice-Op L7-lattice renaming ( _∧_ to _∙∧_ ; _∨_ to _∙∨_ )
∙∧-is-∧-l7 : ∀ (a b : Fin 7) → a ∙∧ b ≡ a ∧ b
∙∧-is-∧-l7 a b = refl
∙∨-is-∨-l7 : ∀ (a b : Fin 7) → a ∙∨ b ≡ a ∨ b
∙∨-is-∨-l7 a b = refl
open Polymorphic.Lattice-Op ⟪ ⟨ L7-lattice ⟩ˡᵃ ⟫ˡᵃ using ()
renaming ( _∧_ to _∙∧'_ ; _∨_ to _∙∨'_ )
roundtrip-∧-l7 : ∀ (a b : Fin 7) → a ∙∧' b ≡ a ∧ b
roundtrip-∧-l7 a b = refl
roundtrip-∨-l7 : ∀ (a b : Fin 7) → a ∙∨' b ≡ a ∨ b
roundtrip-∨-l7 a b = refl
```