---
layout: default
file: "src/Classical/Structures/Lattice/Basic.lagda.md"
title: "Classical.Structures.Lattice.Basic module"
date: "2026-05-28"
author: "the agda-algebras development team"
---
### Lattices {#classical-structures-lattices}
This is the [Classical.Structures.Lattice.Basic][] module of the [Agda Universal Algebra Library][].
This module formalizes a lattice *as an equational algebra*, that is, an algebra
over `Sig-Lattice` satisfying `Th-Lattice`.
For the *order-theoretic* view of a lattice, as a poset with meets and joins (the
form taken by the congruence and subalgebra lattices) see
[Order.CompleteLattice][]. The two presentations are equivalent.
A **lattice** inhabits the Σ-typed structure `Σ[ 𝑨 ∈ Algebra α ρ ] 𝑨 ⊨ Th-Lattice`
over `Sig-Lattice`.
`Lattice`{.AgdaFunction} is the first structure in [`Classical/`][Classical]
with two distinct binary operation symbols (`∧-Op` and `∨-Op`); its signature is
parallel to `Sig-Magma`, not an extension of it, and so it has two natural
forgetful projections, one for each operation, both landing in
[`Semilattice`][Classical.Structures.Semilattice].
This module's adds the following conventions beyond the
[Monoid][Classical.Structures.Monoid] template:
+ **Two reducts, one per operation**.
`lattice→meetMagma` and `lattice→joinMagma` are the two container-morphism
reducts `Sig-Magma ↪ Sig-Lattice` that send `∙-Op` to `∧-Op` and `∨-Op`
respectively, with identity position maps; both are pure reducts (no laws).
`lattice→meetSemilattice` and `lattice→joinSemilattice` add `Th-Semilattice`
satisfaction, just as `monoid→semigroup` does for the single-operation case.
+ **Eight standalone curried laws**.
Each of the eight equations in `Th-Lattice` is exposed as a standalone
lemma (`lt-∧-assoc` through `lt-absorbʳ`), so that both `Lattice-Op` and each
`lattice→<X>Semilattice` consume the same proof.
+ **Direct curried accessors**. `Lattice-Op` defines `_∧_` and `_∨_` directly
rather than inheriting through either semilattice reduct, for the same reason
Monoid does: the reduct's position map re-indexes definitionally to the
identity in both cases, but keeping the accessors direct keeps every downstream
`refl` independent of that reduction.
+ **No two-symbol bridge primitive**. The absorption laws involve terms
nesting two operation symbols
(e.g., `node ∧-Op (pair (ℊ 0F) (node ∨-Op (pair (ℊ 0F) (ℊ 1F))))`);
No new primitive in `Classical.Structures.Interpret` is needed; the existing
`interp-cong` composes through the nesting.
<!--
```agda
{-# OPTIONS --without-K --exact-split --safe #-}
module Classical.Structures.Lattice.Basic where
open import Agda.Primitive using () renaming ( Set to Type )
open import Data.Fin.Base using ( Fin )
open import Data.Fin.Patterns using ( 0F ; 1F ; 2F )
open import Data.Product using ( Σ-syntax ; _×_ ; _,_
; proj₁ ; proj₂ )
open import Function using ( Func )
open import Level using ( Level ; _⊔_ ; suc )
open import Relation.Binary using ( Setoid )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl ; setoid; cong₂)
import Relation.Binary.Reasoning.Setoid as SetoidReasoning
open Func renaming ( to to _⟨$⟩_ )
open import Classical.Operations using ( pair ; Curry₂ )
open import Classical.Signatures.Lattice using ( Sig-Lattice ; Op-Lattice
; ∧-Op ; ∨-Op )
open import Classical.Signatures.Magma using ( Sig-Magma ; Op-Magma )
renaming ( ∙-Op to ∙-Opᵐᵃ )
open import Classical.Structures.Interpret using ( interp-cong )
open import Classical.Structures.Semilattice using ( Semilattice ; _⊨ˢˡ_)
open import Classical.Theories.Lattice using ( Eq-Lattice ; Th-Lattice
; ∧-assoc ; ∧-comm ; ∧-idem
; ∨-assoc ; ∨-comm ; ∨-idem
; absorbˡ ; absorbʳ )
open import Classical.Theories.Semilattice using ( Th-Semilattice )
renaming ( assoc to assocˢˡ
; comm to commˢˡ
; idem to idemˢˡ )
open import Overture.Operations using ( Op )
open import Overture.Terms using ( Term ; ℊ ; node )
open import Overture.Signatures using ( ArityOf ; OperationSymbolsOf )
open import Setoid.Algebras.Basic using ( Algebra ; _^_ ; 𝔻[_] ; 𝕌[_]
; mkAlgebra )
open import Setoid.Algebras.Reduct using ( reductBy )
open import Setoid.Signatures using ( ⟨_⟩ )
open import Setoid.Terms using ( module Environment )
open import Setoid.Varieties.EquationalLogic using ( _⊧_≈_ )
private variable α ρ : Level
```
-->
#### The local satisfaction predicate
```agda
infix 4 _⊨ˡᵃ_
_⊨ˡᵃ_ : (𝑨 : Algebra {𝑆 = Sig-Lattice} α ρ) (ℰ : Eq-Lattice → Term (Fin 3) × Term (Fin 3)) → Type (α ⊔ ρ)
𝑨 ⊨ˡᵃ ℰ = ∀ i → 𝑨 ⊧ proj₁ (ℰ i) ≈ proj₂ (ℰ i)
```
#### The type of lattices
`Lattice α ρ`{.AgdaFunction} pairs an algebra over `Sig-Lattice`{.AgdaFunction} with
a proof of `Th-Lattice`{.AgdaFunction}. Like a ring and unlike a semigroup it needs
its own signature, since meet and join are two operations; and like a ring it has
two reducts to the weaker structure rather than one, one per operation, which is
what the next section constructs.
This is the equational presentation of a lattice. The order-theoretic presentation,
where the two operations are recovered as infimum and supremum of a partial order,
is the one [Setoid.Subalgebras.CompleteLattice][] and
[Setoid.Congruences.CompleteLattice][] use; building order-first is cheaper when the
order is what one has, since the standard library then derives the equations.
```agda
Lattice : (α ρ : Level) → Type (suc α ⊔ suc ρ)
Lattice α ρ = Σ[ 𝑨 ∈ Algebra {𝑆 = Sig-Lattice} α ρ ] 𝑨 ⊨ˡᵃ Th-Lattice
```
#### The meet and join magma reducts
The two container morphisms `Sig-Magma ⟹ Sig-Lattice` send the magma's
`∙-Opᵐᵃ` to the lattice's `∧-Op` and `∨-Op` respectively; the position maps are
the identity (`Fin 2` to `Fin 2`). `lattice→meetMagma` and `lattice→joinMagma`
are the induced reducts.
```agda
∧-incl : Op-Magma → Op-Lattice
∧-incl ∙-Opᵐᵃ = ∧-Op
∧-κ : (o : OperationSymbolsOf Sig-Magma)
→ ArityOf Sig-Lattice (∧-incl o) → ArityOf Sig-Magma o
∧-κ ∙-Opᵐᵃ = λ z → z
∨-incl : Op-Magma → Op-Lattice
∨-incl ∙-Opᵐᵃ = ∨-Op
∨-κ : (o : OperationSymbolsOf Sig-Magma)
→ ArityOf Sig-Lattice (∨-incl o) → ArityOf Sig-Magma o
∨-κ ∙-Opᵐᵃ = λ z → z
lattice→meetMagma : Lattice α ρ → Algebra {𝑆 = Sig-Magma} α ρ
lattice→meetMagma 𝑳 = reductBy ∧-incl ∧-κ (𝑳 .proj₁)
lattice→joinMagma : Lattice α ρ → Algebra {𝑆 = Sig-Magma} α ρ
lattice→joinMagma 𝑳 = reductBy ∨-incl ∨-κ (𝑳 .proj₁)
```
#### Curried laws, standalone
Each of the eight `Th-Lattice` equations is proved here in curried form once,
above the semilattice forgetfuls, so that `Lattice-Op` and each
`lattice→<X>Semilattice` consume the same proof. The pattern is the same as
`Monoid-Op.mn-assoc`: bridge each `node` to curried form via `interp-cong`,
apply the satisfaction-witness equation, refold.
```agda
module _ (𝑳 : Lattice α ρ) where
private 𝑨 = proj₁ 𝑳
open Setoid 𝔻[ 𝑨 ] using (_≈_) renaming (refl to ≈refl; sym to ≈sym; trans to ≈trans)
open Environment 𝑨 using ( ⟦_⟧ )
open SetoidReasoning 𝔻[ 𝑨 ]
private
_∧_ : 𝕌[ 𝑨 ] → 𝕌[ 𝑨 ] → 𝕌[ 𝑨 ]
_∧_ = Curry₂ (∧-Op ^ 𝑨)
_∨_ : 𝕌[ 𝑨 ] → 𝕌[ 𝑨 ] → 𝕌[ 𝑨 ]
_∨_ = Curry₂ (∨-Op ^ 𝑨)
infixl 7 _∧_ _∨_
interp-node-∧ : (s t : Term (Fin 3)) (η : Fin 3 → 𝕌[ 𝑨 ])
→ ⟦ node ∧-Op (pair s t) ⟧ ⟨$⟩ η ≈ ⟦ s ⟧ ⟨$⟩ η ∧ ⟦ t ⟧ ⟨$⟩ η
interp-node-∧ s t η = interp-cong 𝑨 ∧-Op λ { 0F → ≈refl ; 1F → ≈refl }
interp-node-∨ : (s t : Term (Fin 3)) (η : Fin 3 → 𝕌[ 𝑨 ])
→ ⟦ node ∨-Op (pair s t) ⟧ ⟨$⟩ η ≈ ⟦ s ⟧ ⟨$⟩ η ∨ ⟦ t ⟧ ⟨$⟩ η
interp-node-∨ s t η = interp-cong 𝑨 ∨-Op λ { 0F → ≈refl ; 1F → ≈refl }
∧-cong : ∀ {x y u v} → x ≈ y → u ≈ v → x ∧ u ≈ y ∧ v
∧-cong x≈y u≈v = interp-cong 𝑨 ∧-Op λ { 0F → x≈y ; 1F → u≈v }
∨-cong : ∀ {x y u v} → x ≈ y → u ≈ v → x ∨ u ≈ y ∨ v
∨-cong x≈y u≈v = interp-cong 𝑨 ∨-Op λ { 0F → x≈y ; 1F → u≈v }
lt-∧-assoc : ∀ {x y z} → x ∧ y ∧ z ≈ x ∧ (y ∧ z)
lt-∧-assoc {x} {y} {z} = begin
x ∧ y ∧ z ≈˘⟨ ∧-cong (interp-node-∧ (ℊ 0F) (ℊ 1F) η) ≈refl ⟩
⟦ xy ⟧ ⟨$⟩ η ∧ z ≈˘⟨ interp-node-∧ xy (ℊ 2F) η ⟩
⟦ lhsT ⟧ ⟨$⟩ η ≈⟨ proj₂ 𝑳 ∧-assoc η ⟩
⟦ rhsT ⟧ ⟨$⟩ η ≈⟨ interp-node-∧ (ℊ 0F) yz η ⟩
x ∧ ⟦ yz ⟧ ⟨$⟩ η ≈⟨ ∧-cong ≈refl (interp-node-∧ (ℊ 1F) (ℊ 2F) η) ⟩
x ∧ (y ∧ z) ∎
where
η : Fin 3 → 𝕌[ 𝑨 ]
η = λ { 0F → x ; 1F → y ; 2F → z }
xy yz lhsT rhsT : Term (Fin 3)
xy = node ∧-Op (pair (ℊ 0F) (ℊ 1F))
yz = node ∧-Op (pair (ℊ 1F) (ℊ 2F))
lhsT = node ∧-Op (pair xy (ℊ 2F))
rhsT = node ∧-Op (pair (ℊ 0F) yz)
lt-∧-comm : ∀ {x y} → x ∧ y ≈ y ∧ x
lt-∧-comm {x} {y} =
≈trans (≈sym (interp-node-∧ (ℊ 0F) (ℊ 1F) η))
(≈trans (proj₂ 𝑳 ∧-comm η) (interp-node-∧ (ℊ 1F) (ℊ 0F) η))
where
η : Fin 3 → 𝕌[ 𝑨 ]
η = λ { 0F → x ; 1F → y ; 2F → x }
lt-∧-idem : ∀ {x} → x ∧ x ≈ x
lt-∧-idem {x} = ≈trans (≈sym (interp-node-∧ (ℊ 0F) (ℊ 0F) η)) (proj₂ 𝑳 ∧-idem η)
where η : Fin 3 → 𝕌[ 𝑨 ]
η = λ { 0F → x ; 1F → x ; 2F → x }
lt-∨-assoc : ∀ {x y z} → x ∨ y ∨ z ≈ x ∨ (y ∨ z)
lt-∨-assoc {x} {y} {z} = begin
x ∨ y ∨ z ≈˘⟨ ∨-cong (interp-node-∨ (ℊ 0F) (ℊ 1F) η) ≈refl ⟩
⟦ xy ⟧ ⟨$⟩ η ∨ z ≈˘⟨ interp-node-∨ xy (ℊ 2F) η ⟩
⟦ lhsT ⟧ ⟨$⟩ η ≈⟨ proj₂ 𝑳 ∨-assoc η ⟩
⟦ rhsT ⟧ ⟨$⟩ η ≈⟨ interp-node-∨ (ℊ 0F) yz η ⟩
x ∨ ⟦ yz ⟧ ⟨$⟩ η ≈⟨ ∨-cong ≈refl (interp-node-∨ (ℊ 1F) (ℊ 2F) η) ⟩
x ∨ (y ∨ z) ∎
where
η : Fin 3 → 𝕌[ 𝑨 ]
η = λ { 0F → x ; 1F → y ; 2F → z }
xy yz lhsT rhsT : Term (Fin 3)
xy = node ∨-Op (pair (ℊ 0F) (ℊ 1F))
yz = node ∨-Op (pair (ℊ 1F) (ℊ 2F))
lhsT = node ∨-Op (pair xy (ℊ 2F))
rhsT = node ∨-Op (pair (ℊ 0F) yz)
lt-∨-comm : ∀ {x y} → x ∨ y ≈ y ∨ x
lt-∨-comm {x} {y} =
≈trans (≈sym (interp-node-∨ (ℊ 0F) (ℊ 1F) η))
(≈trans (proj₂ 𝑳 ∨-comm η) (interp-node-∨ (ℊ 1F) (ℊ 0F) η))
where
η : Fin 3 → 𝕌[ 𝑨 ]
η = λ { 0F → x ; 1F → y ; 2F → x }
lt-∨-idem : ∀ {x} → x ∨ x ≈ x
lt-∨-idem {x} = ≈trans (≈sym (interp-node-∨ (ℊ 0F) (ℊ 0F) η)) (proj₂ 𝑳 ∨-idem η)
where
η : Fin 3 → 𝕌[ 𝑨 ]
η = λ { 0F → x ; 1F → x ; 2F → x }
lt-absorbˡ : ∀ {x y} → x ∧ (x ∨ y) ≈ x
lt-absorbˡ {x} {y} = begin
x ∧ (x ∨ y) ≈˘⟨ ∧-cong ≈refl (interp-node-∨ (ℊ 0F) (ℊ 1F) η) ⟩
x ∧ ⟦ x∨y ⟧ ⟨$⟩ η ≈˘⟨ interp-node-∧ (ℊ 0F) x∨y η ⟩
⟦ lhsT ⟧ ⟨$⟩ η ≈⟨ proj₂ 𝑳 absorbˡ η ⟩
x ∎
where
η : Fin 3 → 𝕌[ 𝑨 ]
η = λ { 0F → x ; 1F → y ; 2F → x }
x∨y lhsT : Term (Fin 3)
x∨y = node ∨-Op (pair (ℊ 0F) (ℊ 1F))
lhsT = node ∧-Op (pair (ℊ 0F) x∨y)
lt-absorbʳ : ∀ {x y} → (x ∧ y) ∨ x ≈ x
lt-absorbʳ {x} {y} = begin
(x ∧ y) ∨ x ≈˘⟨ ∨-cong (interp-node-∧ (ℊ 0F) (ℊ 1F) η) ≈refl ⟩
⟦ x∧y ⟧ ⟨$⟩ η ∨ x ≈˘⟨ interp-node-∨ x∧y (ℊ 0F) η ⟩
⟦ lhsT ⟧ ⟨$⟩ η ≈⟨ proj₂ 𝑳 absorbʳ η ⟩
x ∎
where
η : Fin 3 → 𝕌[ 𝑨 ]
η = λ { 0F → x ; 1F → y ; 2F → x }
x∧y lhsT : Term (Fin 3)
x∧y = node ∧-Op (pair (ℊ 0F) (ℊ 1F))
lhsT = node ∨-Op (pair x∧y (ℊ 0F))
```
#### The `Lattice-Op` module
`Lattice-Op` exposes `_∧_`, `_∨_`, their congruences, the term-to-curried node
bridges `interp-node-∧` / `interp-node-∨`, the eight curried laws (matching the
eight constructors of `Eq-Lattice`), and the satisfaction-witness `equations`
accessor.
```agda
module Lattice-Op {α ρ : Level} (𝑳 : Lattice α ρ) where
private 𝑨 = proj₁ 𝑳
open Setoid 𝔻[ 𝑨 ] using (_≈_) renaming (refl to ≈refl)
open Environment 𝑨 using ( ⟦_⟧ )
infixl 7 _∧_ _∨_
_∧_ : 𝕌[ 𝑨 ] → 𝕌[ 𝑨 ] → 𝕌[ 𝑨 ]
_∧_ = Curry₂ (∧-Op ^ 𝑨)
_∨_ : 𝕌[ 𝑨 ] → 𝕌[ 𝑨 ] → 𝕌[ 𝑨 ]
_∨_ = Curry₂ (∨-Op ^ 𝑨)
equations : 𝑨 ⊨ˡᵃ Th-Lattice
equations = proj₂ 𝑳
∧-cong : ∀ {x y u v} → x ≈ y → u ≈ v → x ∧ u ≈ y ∧ v
∧-cong x≈y u≈v = interp-cong 𝑨 ∧-Op λ { 0F → x≈y ; 1F → u≈v }
∨-cong : ∀ {x y u v} → x ≈ y → u ≈ v → x ∨ u ≈ y ∨ v
∨-cong x≈y u≈v = interp-cong 𝑨 ∨-Op λ { 0F → x≈y ; 1F → u≈v }
interp-node-∧ : (s t : Term (Fin 3)) {η : Fin 3 → 𝕌[ 𝑨 ]}
→ ⟦ node ∧-Op (pair s t) ⟧ ⟨$⟩ η ≈ ⟦ s ⟧ ⟨$⟩ η ∧ ⟦ t ⟧ ⟨$⟩ η
interp-node-∧ s t = interp-cong 𝑨 ∧-Op λ { 0F → ≈refl ; 1F → ≈refl }
interp-node-∨ : (s t : Term (Fin 3)) {η : Fin 3 → 𝕌[ 𝑨 ]}
→ ⟦ node ∨-Op (pair s t) ⟧ ⟨$⟩ η ≈ ⟦ s ⟧ ⟨$⟩ η ∨ ⟦ t ⟧ ⟨$⟩ η
interp-node-∨ s t = interp-cong 𝑨 ∨-Op λ { 0F → ≈refl ; 1F → ≈refl }
∧-assoc-law : ∀ {x y z} → x ∧ y ∧ z ≈ x ∧ (y ∧ z)
∧-assoc-law = lt-∧-assoc 𝑳
∧-comm-law : ∀ {x y} → x ∧ y ≈ y ∧ x
∧-comm-law = lt-∧-comm 𝑳
∧-idem-law : ∀ {x} → x ∧ x ≈ x
∧-idem-law = lt-∧-idem 𝑳
∨-assoc-law : ∀ {x y z} → x ∨ y ∨ z ≈ x ∨ (y ∨ z)
∨-assoc-law = lt-∨-assoc 𝑳
∨-comm-law : ∀ {x y} → x ∨ y ≈ y ∨ x
∨-comm-law = lt-∨-comm 𝑳
∨-idem-law : ∀ {x} → x ∨ x ≈ x
∨-idem-law = lt-∨-idem 𝑳
absorbˡ-law : ∀ {x y} → x ∧ (x ∨ y) ≈ x
absorbˡ-law = lt-absorbˡ 𝑳
absorbʳ-law : ∀ {x y} → (x ∧ y) ∨ x ≈ x
absorbʳ-law = lt-absorbʳ 𝑳
```
#### The forgetful projections to semilattices
`lattice→meetSemilattice` and `lattice→joinSemilattice` each take a lattice to
the semilattice on its meet (resp. join) operation: the underlying algebra is
the corresponding magma reduct, and the `Th-Semilattice` satisfaction proof
pivots through `lt-∧-{assoc,comm,idem}` (resp. `lt-∨-{assoc,comm,idem}`) by
the curried-law-pivot pattern of `monoid→semigroup`.
```agda
lattice→meetSemilattice : Lattice α ρ → Semilattice α ρ
lattice→meetSemilattice ℒ@(𝑳 , _) = 𝑹 , thm
where
𝑹 : Algebra {𝑆 = Sig-Magma} _ _
𝑹 = lattice→meetMagma ℒ
open Setoid 𝔻[ 𝑳 ] using (_≈_) renaming (refl to ≈refl)
open Environment 𝑹 using ( ⟦_⟧ )
open SetoidReasoning 𝔻[ 𝑳 ]
open Lattice-Op ℒ using ( _∧_ ; ∧-assoc-law ; ∧-comm-law ; ∧-idem-law )
interp-congᴿ : (s t : Term (Fin 3)) (η : Fin 3 → 𝕌[ 𝑳 ])
→ ⟦ node ∙-Opᵐᵃ (pair s t) ⟧ ⟨$⟩ η ≈ (⟦ s ⟧ ⟨$⟩ η) ∧ (⟦ t ⟧ ⟨$⟩ η)
interp-congᴿ s t η = interp-cong 𝑹 ∙-Opᵐᵃ λ { 0F → ≈refl ; 1F → ≈refl }
∧-congᴿ : ∀ {a b c d} → a ≈ b → c ≈ d → a ∧ c ≈ b ∧ d
∧-congᴿ a≈b c≈d = interp-cong 𝑹 ∙-Opᵐᵃ λ { 0F → a≈b ; 1F → c≈d }
thm : 𝑹 ⊨ˢˡ Th-Semilattice
thm assocˢˡ η = let x = η 0F ; y = η 1F ; z = η 2F in begin
⟦ Th-Semilattice assocˢˡ .proj₁ ⟧ ⟨$⟩ η ≈⟨ interp-congᴿ xy (ℊ 2F) η ⟩
⟦ xy ⟧ ⟨$⟩ η ∧ z ≈⟨ ∧-congᴿ (interp-congᴿ (ℊ 0F) (ℊ 1F) η) ≈refl ⟩
(x ∧ y) ∧ z ≈⟨ ∧-assoc-law ⟩
x ∧ (y ∧ z) ≈˘⟨ ∧-congᴿ ≈refl (interp-congᴿ (ℊ 1F) (ℊ 2F) η) ⟩
x ∧ ⟦ yz ⟧ ⟨$⟩ η ≈˘⟨ interp-congᴿ (ℊ 0F) yz η ⟩
⟦ Th-Semilattice assocˢˡ .proj₂ ⟧ ⟨$⟩ η ∎
where
xy yz : Term (Fin 3)
xy = node ∙-Opᵐᵃ (pair (ℊ 0F) (ℊ 1F))
yz = node ∙-Opᵐᵃ (pair (ℊ 1F) (ℊ 2F))
thm commˢˡ η = let x = η 0F ; y = η 1F in begin
⟦ Th-Semilattice commˢˡ .proj₁ ⟧ ⟨$⟩ η ≈⟨ interp-congᴿ (ℊ 0F) (ℊ 1F) η ⟩
x ∧ y ≈⟨ ∧-comm-law ⟩
y ∧ x ≈˘⟨ interp-congᴿ (ℊ 1F) (ℊ 0F) η ⟩
⟦ Th-Semilattice commˢˡ .proj₂ ⟧ ⟨$⟩ η ∎
thm idemˢˡ η = let x = η 0F in begin
⟦ Th-Semilattice idemˢˡ .proj₁ ⟧ ⟨$⟩ η ≈⟨ interp-congᴿ (ℊ 0F) (ℊ 0F) η ⟩
x ∧ x ≈⟨ ∧-idem-law ⟩
x ∎
lattice→joinSemilattice : Lattice α ρ → Semilattice α ρ
lattice→joinSemilattice ℒ@(𝑳 , _) = 𝑹 , thm
where
𝑹 : Algebra {𝑆 = Sig-Magma} _ _
𝑹 = lattice→joinMagma ℒ
open Setoid 𝔻[ 𝑳 ] using (_≈_) renaming (refl to ≈refl)
open Environment 𝑹 using ( ⟦_⟧ )
open SetoidReasoning 𝔻[ 𝑳 ]
open Lattice-Op ℒ using ( _∨_ ; ∨-assoc-law ; ∨-comm-law ; ∨-idem-law )
interp-congᴿ : (s t : Term (Fin 3)) (η : Fin 3 → 𝕌[ 𝑳 ])
→ ⟦ node ∙-Opᵐᵃ (pair s t) ⟧ ⟨$⟩ η ≈ ⟦ s ⟧ ⟨$⟩ η ∨ ⟦ t ⟧ ⟨$⟩ η
interp-congᴿ s t η = interp-cong 𝑹 ∙-Opᵐᵃ λ { 0F → ≈refl ; 1F → ≈refl }
∨-congᴿ : ∀ {a b c d} → a ≈ b → c ≈ d → a ∨ c ≈ b ∨ d
∨-congᴿ a≈b c≈d = interp-cong 𝑹 ∙-Opᵐᵃ λ { 0F → a≈b ; 1F → c≈d }
thm : 𝑹 ⊨ˢˡ Th-Semilattice
thm assocˢˡ η = let x = η 0F ; y = η 1F ; z = η 2F in begin
⟦ Th-Semilattice assocˢˡ .proj₁ ⟧ ⟨$⟩ η ≈⟨ interp-congᴿ xy (ℊ 2F) η ⟩
⟦ xy ⟧ ⟨$⟩ η ∨ z ≈⟨ ∨-congᴿ (interp-congᴿ (ℊ 0F) (ℊ 1F) η) ≈refl ⟩
(x ∨ y) ∨ z ≈⟨ ∨-assoc-law ⟩
x ∨ (y ∨ z) ≈˘⟨ ∨-congᴿ ≈refl (interp-congᴿ (ℊ 1F) (ℊ 2F) η) ⟩
x ∨ ⟦ yz ⟧ ⟨$⟩ η ≈˘⟨ interp-congᴿ (ℊ 0F) yz η ⟩
⟦ Th-Semilattice assocˢˡ .proj₂ ⟧ ⟨$⟩ η ∎
where
xy yz : Term (Fin 3)
xy = node ∙-Opᵐᵃ (pair (ℊ 0F) (ℊ 1F))
yz = node ∙-Opᵐᵃ (pair (ℊ 1F) (ℊ 2F))
thm commˢˡ η = let x = η 0F ; y = η 1F in begin
⟦ Th-Semilattice commˢˡ .proj₁ ⟧ ⟨$⟩ η ≈⟨ interp-congᴿ (ℊ 0F) (ℊ 1F) η ⟩
x ∨ y ≈⟨ ∨-comm-law ⟩
y ∨ x ≈˘⟨ interp-congᴿ (ℊ 1F) (ℊ 0F) η ⟩
⟦ Th-Semilattice commˢˡ .proj₂ ⟧ ⟨$⟩ η ∎
thm idemˢˡ η = let x = η 0F in begin
⟦ Th-Semilattice idemˢˡ .proj₁ ⟧ ⟨$⟩ η ≈⟨ interp-congᴿ (ℊ 0F) (ℊ 0F) η ⟩
x ∨ x ≈⟨ ∨-idem-law ⟩
x ∎
```
#### Lattice builders
`opsToBareLattice` builds a "raw" `Sig-Lattice`-algebra from a carrier and two
binary operations. `eqsToLattice` adds the eight equation proofs and produces
a `Lattice α α`.
```agda
open Algebra
opsToBareLattice : (A : Type α) (_∧'_ _∨'_ : A → A → A) → Algebra {𝑆 = Sig-Lattice} α α
opsToBareLattice A _∧'_ _∨'_ .Domain = setoid A
opsToBareLattice A _∧'_ _∨'_ .Interp ⟨$⟩ (∧-Op , args) = args 0F ∧' args 1F
opsToBareLattice A _∧'_ _∨'_ .Interp ⟨$⟩ (∨-Op , args) = args 0F ∨' args 1F
opsToBareLattice A _∧'_ _∨'_ .Interp .cong {∧-Op , _} {.∧-Op , _} (refl , args≡) = cong₂ _∧'_ (args≡ 0F) (args≡ 1F)
opsToBareLattice A _∧'_ _∨'_ .Interp .cong {∨-Op , _} {.∨-Op , _} (refl , args≡) = cong₂ _∨'_ (args≡ 0F) (args≡ 1F)
eqsToLattice : (A : Type α) (_∧'_ _∨'_ : A → A → A)
→ (∧-assoc-≡ : ∀ a b c → (a ∧' b) ∧' c ≡ a ∧' (b ∧' c))
→ (∧-comm-≡ : ∀ a b → a ∧' b ≡ b ∧' a)
→ (∧-idem-≡ : ∀ a → a ∧' a ≡ a)
→ (∨-assoc-≡ : ∀ a b c → (a ∨' b) ∨' c ≡ a ∨' (b ∨' c))
→ (∨-comm-≡ : ∀ a b → a ∨' b ≡ b ∨' a)
→ (∨-idem-≡ : ∀ a → a ∨' a ≡ a)
→ (absorbˡ-≡ : ∀ a b → a ∧' (a ∨' b) ≡ a)
→ (absorbʳ-≡ : ∀ a b → (a ∧' b) ∨' a ≡ a)
→ Lattice α α
eqsToLattice A _∧'_ _∨'_ ∧-assoc-≡ ∧-comm-≡ ∧-idem-≡ ∨-assoc-≡ ∨-comm-≡ ∨-idem-≡ absorbˡ-≡ absorbʳ-≡ =
opsToBareLattice A _∧'_ _∨'_ , proof
where
proof : opsToBareLattice A _∧'_ _∨'_ ⊨ˡᵃ Th-Lattice
proof ∧-assoc ρ = ∧-assoc-≡ (ρ 0F) (ρ 1F) (ρ 2F)
proof ∧-comm ρ = ∧-comm-≡ (ρ 0F) (ρ 1F)
proof ∧-idem ρ = ∧-idem-≡ (ρ 0F)
proof ∨-assoc ρ = ∨-assoc-≡ (ρ 0F) (ρ 1F) (ρ 2F)
proof ∨-comm ρ = ∨-comm-≡ (ρ 0F) (ρ 1F)
proof ∨-idem ρ = ∨-idem-≡ (ρ 0F)
proof absorbˡ ρ = absorbˡ-≡ (ρ 0F) (ρ 1F)
proof absorbʳ ρ = absorbʳ-≡ (ρ 0F) (ρ 1F)
```
#### Setoid-level lattice builders
`eqsToLattice`{.AgdaFunction} covers carriers with propositional equality; the
constructions that build one lattice out of others (the binary product, the dual,
and the ordinal sum of [Classical.Structures.Lattice.Product][],
[Classical.Structures.Lattice.Dual][], and
[Classical.Structures.Lattice.OrdinalSum][]) produce *setoid* carriers, so they
need the general form.
`setoidOpsToBareLattice`{.AgdaFunction} assembles the `Sig-Lattice` algebra from a
carrier setoid, two binary operations, and their congruence proofs (which the
propositional case got for free from `cong₂`{.AgdaFunction});
`setoidEqsToLattice`{.AgdaFunction} adds the eight equations, now stated over the
setoid equality `≈`.
The interpretation clauses apply the argument tuple (`a 0F ∧' a 1F` rather than
routing through `pair`{.AgdaFunction}), so each equation of `Th-Lattice` evaluates
definitionally to its curried form, and the satisfaction proof consumes the
curried hypotheses directly (the same reduction discipline that makes
`eqsToLattice`{.AgdaFunction}'s proof clauses one-liners).
```agda
module _ (𝐷 : Setoid α ρ) where
open Setoid 𝐷 using ( _≈_ ) renaming ( Carrier to D )
setoidOpsToBareLattice : (_∧'_ _∨'_ : D → D → D)
→ (∀ {x y u v} → x ≈ y → u ≈ v → (x ∧' u) ≈ (y ∧' v))
→ (∀ {x y u v} → x ≈ y → u ≈ v → (x ∨' u) ≈ (y ∨' v))
→ Algebra {𝑆 = Sig-Lattice} α ρ
setoidOpsToBareLattice _∧'_ _∨'_ ∧'-cong ∨'-cong = mkAlgebra 𝐷 interp interp-congruence
where
interp : (o : OperationSymbolsOf Sig-Lattice) → Op (ArityOf Sig-Lattice o) D
interp ∧-Op a = a 0F ∧' a 1F
interp ∨-Op a = a 0F ∨' a 1F
interp-congruence : ∀ o {u v : ArityOf Sig-Lattice o → D}
→ (∀ i → u i ≈ v i) → interp o u ≈ interp o v
interp-congruence ∧-Op e = ∧'-cong (e 0F) (e 1F)
interp-congruence ∨-Op e = ∨'-cong (e 0F) (e 1F)
setoidEqsToLattice : (_∧'_ _∨'_ : D → D → D)
→ (∧'-cong : ∀ {x y u v} → x ≈ y → u ≈ v → (x ∧' u) ≈ (y ∧' v))
→ (∨'-cong : ∀ {x y u v} → x ≈ y → u ≈ v → (x ∨' u) ≈ (y ∨' v))
→ (∧'-assoc-≈ : ∀ {a b c} → ((a ∧' b) ∧' c) ≈ (a ∧' (b ∧' c)))
→ (∧'-comm-≈ : ∀ {a b} → (a ∧' b) ≈ (b ∧' a))
→ (∧'-idem-≈ : ∀ {a} → (a ∧' a) ≈ a)
→ (∨'-assoc-≈ : ∀ {a b c} → ((a ∨' b) ∨' c) ≈ (a ∨' (b ∨' c)))
→ (∨'-comm-≈ : ∀ {a b} → (a ∨' b) ≈ (b ∨' a))
→ (∨'-idem-≈ : ∀ {a} → (a ∨' a) ≈ a)
→ (absorbˡ-≈ : ∀ {a b} → (a ∧' (a ∨' b)) ≈ a)
→ (absorbʳ-≈ : ∀ {a b} → ((a ∧' b) ∨' a) ≈ a)
→ Lattice α ρ
setoidEqsToLattice _∧'_ _∨'_ ∧'-cong ∨'-cong
∧'-assoc-≈ ∧'-comm-≈ ∧'-idem-≈ ∨'-assoc-≈ ∨'-comm-≈ ∨'-idem-≈ absorbˡ-≈ absorbʳ-≈ =
setoidOpsToBareLattice _∧'_ _∨'_ ∧'-cong ∨'-cong , proof
where
proof : setoidOpsToBareLattice _∧'_ _∨'_ ∧'-cong ∨'-cong ⊨ˡᵃ Th-Lattice
proof ∧-assoc η = ∧'-assoc-≈
proof ∧-comm η = ∧'-comm-≈
proof ∧-idem η = ∧'-idem-≈
proof ∨-assoc η = ∨'-assoc-≈
proof ∨-comm η = ∨'-comm-≈
proof ∨-idem η = ∨'-idem-≈
proof absorbˡ η = absorbˡ-≈
proof absorbʳ η = absorbʳ-≈
```