---
layout: default
file: "src/Classical/Structures/Lattice/Product.lagda.md"
title: "Classical.Structures.Lattice.Product module"
date: "2026-07-24"
author: "the agda-algebras development team"
---
### Binary products of lattices {#classical-structures-lattice-product}
This is the [Classical.Structures.Lattice.Product][] module of the [Agda Universal Algebra Library][].
Given lattices `π³β`{.AgdaBound} and `π³β`{.AgdaBound} over
[`Sig-Lattice`][Classical.Signatures.Lattice], this module constructs their
**binary direct product** `π³β`{.AgdaBound}` ΓΛ‘ `{.AgdaFunction}`π³β`{.AgdaBound}:
the lattice on the product
setoid whose meet and join act componentwise. The construction mirrors the group
case ([Classical.Structures.Group.Product][]) but is assembled through the
setoid-level builder `setoidEqsToLattice`{.AgdaFunction} of
[Classical.Structures.Lattice][], whose interpretation clauses reduce
definitionally; consequently each of the eight lattice equations for the product is
*literally* the pair of the component equations, and no term-induction lemma is
needed.
Besides the product itself, the module characterizes the induced meet order of
[Classical.Properties.Lattice][]: the product order is the componentwise order,
definitionally, and the three accessors `β€β-fst`{.AgdaFunction},
`β€β-snd`{.AgdaFunction}, `β€β-pair`{.AgdaFunction} name the two projections and the
pairing. The first consumer is the FLRP closure toolkit
([FLRP.Closure][]; roadmap Β§ 3, work package WP-5), which represents
`π³β ΓΛ‘ π³β`{.AgdaFunction} as a congruence lattice whenever its factors are so
representable.
Following the Cubical-port discipline, the underlying equivalence of the product is
isolated in `AΓB`{.AgdaFunction} β the pointwise pair of the component
equivalences β so it can be mechanically substituted on the eventual port.
<!--
```agda
{-# OPTIONS --cubical-compatible --exact-split --safe #-}
module Classical.Structures.Lattice.Product where
open import Data.Product using ( _,_ ; _Γ_ ; projβ ; projβ )
open import Level using ( Level ; _β_ )
open import Relation.Binary using ( Setoid )
open import Classical.Properties.Lattice using ( module Lattice-Order )
open import Classical.Structures.Lattice.Basic using ( Lattice ; module Lattice-Op
; setoidEqsToLattice )
open import Setoid.Algebras.Basic using ( π[_] ; π»[_] )
private variable Ξ± Ο Ξ² Ο : Level
```
-->
#### The product construction
`LatticeProduct`{.AgdaModule} `π³β` `π³β` packages the whole development for a fixed
pair of lattices; opening it provides the product setoid, the componentwise
operations with their congruences and equations, the product lattice, and the
characterization of its order.
```agda
module LatticeProduct (π³β : Lattice Ξ± Ο) (π³β : Lattice Ξ² Ο) where
private
π¨ = projβ π³β
π© = projβ π³β
open Setoid π»[ π¨ ] using ()
renaming ( _β_ to _ββ_ ; refl to reflβ ; sym to symβ ; trans to transβ )
open Setoid π»[ π© ] using ()
renaming ( _β_ to _ββ_ ; refl to reflβ ; sym to symβ ; trans to transβ )
open Lattice-Op π³β using ()
renaming ( _β§_ to _β§β_ ; _β¨_ to _β¨β_ ; β§-cong to β§β-cong ; β¨-cong to β¨β-cong
; β§-assoc-law to β§β-assoc ; β§-comm-law to β§β-comm ; β§-idem-law to β§β-idem
; β¨-assoc-law to β¨β-assoc ; β¨-comm-law to β¨β-comm ; β¨-idem-law to β¨β-idem
; absorbΛ‘-law to absorbΛ‘β ; absorbΚ³-law to absorbΚ³β )
open Lattice-Op π³β using ()
renaming ( _β§_ to _β§β_ ; _β¨_ to _β¨β_ ; β§-cong to β§β-cong ; β¨-cong to β¨β-cong
; β§-assoc-law to β§β-assoc ; β§-comm-law to β§β-comm ; β§-idem-law to β§β-idem
; β¨-assoc-law to β¨β-assoc ; β¨-comm-law to β¨β-comm ; β¨-idem-law to β¨β-idem
; absorbΛ‘-law to absorbΛ‘β ; absorbΚ³-law to absorbΚ³β )
```
The carrier of the product is the pair type, and its equivalence is the pointwise
pair of the component equivalences β the isolated-equality locus for the Cubical
port.
```agda
AΓB : Setoid (Ξ± β Ξ²) (Ο β Ο)
AΓB = record
{ Carrier = π[ π¨ ] Γ π[ π© ]
; _β_ = Ξ» p q β (projβ p ββ projβ q) Γ (projβ p ββ projβ q)
; isEquivalence = record
{ refl = reflβ , reflβ
; sym = Ξ» e β symβ (projβ e) , symβ (projβ e)
; trans = Ξ» (dβ , dβ) (eβ , eβ) β transβ dβ eβ , transβ dβ eβ
}
}
open Setoid AΓB using () renaming ( _β_ to _ββ_ )
```
Meet and join act componentwise. The operations project rather than pattern-match
their arguments, so they reduce on any pair expression, matched or not.
```agda
_β§β_ : π[ π¨ ] Γ π[ π© ] β π[ π¨ ] Γ π[ π© ] β π[ π¨ ] Γ π[ π© ]
p β§β q = (projβ p β§β projβ q) , (projβ p β§β projβ q)
_β¨β_ : π[ π¨ ] Γ π[ π© ] β π[ π¨ ] Γ π[ π© ] β π[ π¨ ] Γ π[ π© ]
p β¨β q = (projβ p β¨β projβ q) , (projβ p β¨β projβ q)
```
Congruence and the eight equations are all inherited componentwise: each proof is
the pair of the component proofs, applied at the projections.
```agda
β§β-cong : β {p q u v} β p ββ q β u ββ v β (p β§β u) ββ (q β§β v)
β§β-cong e f = β§β-cong (projβ e) (projβ f) , β§β-cong (projβ e) (projβ f)
β¨β-cong : β {p q u v} β p ββ q β u ββ v β (p β¨β u) ββ (q β¨β v)
β¨β-cong e f = β¨β-cong (projβ e) (projβ f) , β¨β-cong (projβ e) (projβ f)
β§β-assoc : β {p q r} β ((p β§β q) β§β r) ββ (p β§β (q β§β r))
β§β-assoc = β§β-assoc , β§β-assoc
β§β-comm : β {p q} β (p β§β q) ββ (q β§β p)
β§β-comm = β§β-comm , β§β-comm
β§β-idem : β {p} β (p β§β p) ββ p
β§β-idem = β§β-idem , β§β-idem
β¨β-assoc : β {p q r} β ((p β¨β q) β¨β r) ββ (p β¨β (q β¨β r))
β¨β-assoc = β¨β-assoc , β¨β-assoc
β¨β-comm : β {p q} β (p β¨β q) ββ (q β¨β p)
β¨β-comm = β¨β-comm , β¨β-comm
β¨β-idem : β {p} β (p β¨β p) ββ p
β¨β-idem = β¨β-idem , β¨β-idem
absorbΛ‘β : β {p q} β (p β§β (p β¨β q)) ββ p
absorbΛ‘β = absorbΛ‘β , absorbΛ‘β
absorbΚ³β : β {p q} β ((p β§β q) β¨β p) ββ p
absorbΚ³β = absorbΚ³β , absorbΚ³β
```
Assembling through the setoid-level builder yields the product lattice.
```agda
ΓΛ‘-Lattice : Lattice (Ξ± β Ξ²) (Ο β Ο)
ΓΛ‘-Lattice = setoidEqsToLattice AΓB _β§β_ _β¨β_ β§β-cong β¨β-cong
β§β-assoc β§β-comm β§β-idem β¨β-assoc β¨β-comm β¨β-idem absorbΛ‘β absorbΚ³β
```
#### The product order is the componentwise order
The meet order of `ΓΛ‘-Lattice`{.AgdaFunction} at `(p , q)` unfolds definitionally
to the pair of the component meet orders, because the builder's interpretation
applies its argument tuple and the product setoid's equality is the pointwise pair.
The three accessors below are therefore projections and pairing, but we name them:
they are the interface through which consumers (the FLRP closure lemmas) read the
product order without unfolding the builder.
```agda
open Lattice-Order ΓΛ‘-Lattice using () renaming ( _β€_ to _β€β_ )
open Lattice-Order π³β using () renaming ( _β€_ to _β€β_ )
open Lattice-Order π³β using () renaming ( _β€_ to _β€β_ )
β€β-fst : β {p q} β p β€β q β projβ p β€β projβ q
β€β-fst = projβ
β€β-snd : β {p q} β p β€β q β projβ p β€β projβ q
β€β-snd = projβ
β€β-pair : β {p q} β projβ p β€β projβ q β projβ p β€β projβ q β p β€β q
β€β-pair e f = e , f
```
#### The product operator
The standalone binary operator, for consumers that need only the lattice.
```agda
infixr 7 _ΓΛ‘_
_ΓΛ‘_ : Lattice Ξ± Ο β Lattice Ξ² Ο β Lattice (Ξ± β Ξ²) (Ο β Ο)
π³β ΓΛ‘ π³β = LatticeProduct.ΓΛ‘-Lattice π³β π³β
```
--------------------------------------