---
layout: default
title : "Setoid.Subalgebras.CompleteLattice module (The Agda Universal Algebra Library)"
date : "2026-06-02"
author: "agda-algebras development team"
---
### The Complete Lattice of Subuniverses
This is the [Setoid.Subalgebras.CompleteLattice][] module of the [Agda Universal Algebra Library][].
The subuniverses of a setoid algebra `𝑨` (the subsets of its carrier closed under
the basic operations) form a **complete lattice** `Sub 𝑨` under inclusion.
This is the second instance of the order-theoretic `CompleteLattice` record of
[Order.CompleteLattice][] (the first being the congruence lattice
[Setoid.Congruences.CompleteLattice][]), and it is built directly from the
subuniverse-generation machinery of [Setoid.Subalgebras.Subuniverses][].
+ `Subuniverses 𝑨`: the predicate "is a subuniverse";
+ `Sg 𝑨 G`: the subuniverse generated by `G`, with `sgIsSub` (it is a subuniverse)
and `sgIsSmallest` (it is the *least* subuniverse containing `G`);
+ `⋂s`: an arbitrary intersection of subuniverses is a subuniverse.
As with the congruence lattice, the join generated by `Sg` raises the predicate
level from `ℓ` to `𝓞 ⊔ 𝓥 ⊔ α ⊔ ℓ`, so we evaluate the lattice at the absorbing
level `L = 𝓞 ⊔ 𝓥 ⊔ α ⊔ ℓ₀`, at which `Sg` (and the infinitary `⋃`/`⋂` over
`ℓ₀`-small families) stays at `L`. (Unlike congruences there is no `ρ`, since a
subuniverse is a predicate on the carrier and does not mention the setoid
equality.)
<!--
```agda
{-# OPTIONS --cubical-compatible --exact-split --safe #-}
module Setoid.Subalgebras.CompleteLattice where
open import Agda.Primitive using () renaming ( Set to Type )
open import Data.Empty using ( ⊥ )
open import Data.Product using ( _,_ ; _×_ ; proj₁ ; proj₂ ; Σ-syntax )
open import Data.Sum.Base using ( inj₁ ; inj₂ )
open import Data.Unit.Base using ( ⊤ ; tt )
open import Level using ( Level ; _⊔_ ; Lift ; lift )
open import Relation.Binary using ( IsEquivalence ; IsPartialOrder )
open import Relation.Binary.Definitions using ( Maximum ; Minimum )
open import Relation.Binary.Lattice using ( Supremum ; Infimum ; IsLattice
; Lattice ; IsBoundedLattice
; BoundedLattice )
open import Relation.Unary using ( Pred ; _∈_ ; _⊆_ ; _∩_ ; _∪_ ; ⋂ ; ⋃ )
open import Overture using ( 𝓞 ; 𝓥 ; Signature ; 𝑆 )
open import Setoid.Algebras.Basic using ( ov ; Algebra ; 𝕌[_] )
open import Order.CompleteLattice using ( CompleteLattice )
open import Setoid.Subalgebras.Subuniverses using ( Subuniverses ; Sg ; var
; sgIsSub ; sgIsSmallest ; ⋂s )
private variable α ρᵃ : Level
```
-->
#### The subuniverse lattice at the absorbing level `L`
The subuniverse lattice of an algebra is formalized here and packaged inside a module
called `Sublattice`, which is parametrized by the algebra `𝑨` and a base level `ℓ₀`.
This way opening the `Sublattice` module at a use site (with, e.g., `open Sublattice 𝑨 ℓ₀`)
makes available `_≤_`, `_∧_`, `_∨_`, the bounds, and the bundles specialized to `𝑨`.
One can then write `B ≤ C`, instead of `_≤_ 𝑨 ℓ₀ B C`.
```agda
module Sublattice {𝓞 𝓥 : Level}{𝑆 : Signature 𝓞 𝓥}(𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ) (ℓ₀ : Level) where
private A = 𝕌[ 𝑨 ]
L : Level
L = 𝓞 ⊔ 𝓥 ⊔ α ⊔ ℓ₀
Subᴸ : Type (α ⊔ ov {𝑆 = 𝑆} L)
Subᴸ = Σ[ B ∈ Pred A L ] B ∈ Subuniverses 𝑨
```
The order is inclusion of the underlying predicates, and the associated equality is
mutual inclusion.
```agda
infix 4 _≤_ _≈_
_≤_ : Subᴸ → Subᴸ → Type (α ⊔ L)
B ≤ C = proj₁ B ⊆ proj₁ C
_≈_ : Subᴸ → Subᴸ → Type (α ⊔ L)
B ≈ C = (B ≤ C) × (C ≤ B)
≈-isEquivalence : IsEquivalence _≈_
≈-isEquivalence = record
{ refl = (λ z → z) , (λ z → z)
; sym = λ (p , q) → q , p
; trans = λ (p , q) (p′ , q′) → (λ z → p′ (p z)) , (λ z → q (q′ z))
}
≤-isPartialOrder : IsPartialOrder _≈_ _≤_
≤-isPartialOrder = record
{ isPreorder = record { isEquivalence = ≈-isEquivalence
; reflexive = proj₁
; trans = λ p q z → q (p z)
}
; antisym = λ p q → p , q
}
```
#### Meet and join
The meet is the intersection of the underlying predicates (a subuniverse,
componentwise), and the join is the subuniverse *generated* by the union.
```agda
infixr 7 _∧_
infixr 6 _∨_
_∧_ : Subᴸ → Subᴸ → Subᴸ
B ∧ C = (proj₁ B ∩ proj₁ C)
, λ f a im → proj₂ B f a (λ i → proj₁ (im i))
, proj₂ C f a (λ i → proj₂ (im i))
_∨_ : Subᴸ → Subᴸ → Subᴸ
B ∨ C = Sg 𝑨 (proj₁ B ∪ proj₁ C) , sgIsSub 𝑨
∧-infimum : Infimum _≤_ _∧_
∧-infimum B C = (λ z → proj₁ z)
, (λ z → proj₂ z)
, λ D D≤B D≤C z → D≤B z , D≤C z
∨-supremum : Supremum _≤_ _∨_
∨-supremum B C = (λ z → var (inj₁ z))
, (λ z → var (inj₂ z))
, λ D B≤D C≤D → sgIsSmallest 𝑨 (proj₁ D) (proj₂ D)
(λ { (inj₁ x) → B≤D x ; (inj₂ x) → C≤D x })
```
#### The lattice
With the partial order and both binary bounds in hand, the lattice structure is
just assembly. `Sub-isLattice`{.AgdaFunction} packages
`≤-isPartialOrder`{.AgdaFunction}, `∨-supremum`{.AgdaFunction} and
`∧-infimum`{.AgdaFunction} as the standard library's `IsLattice`{.AgdaRecord}, and
`Sub-Lattice`{.AgdaFunction} bundles that together with the carrier and the two
operations as a `Lattice`{.AgdaRecord}.
Building the lattice order-first, from the infimum and supremum rather than from
the lattice identities, is deliberate. The standard library derives the
absorption and associativity laws, and their congruences, from the order, so none
of them has to be proved here.
```agda
Sub-isLattice : IsLattice _≈_ _≤_ _∨_ _∧_
Sub-isLattice = record { isPartialOrder = ≤-isPartialOrder
; supremum = ∨-supremum
; infimum = ∧-infimum
}
Sub-Lattice : Lattice (α ⊔ ov {𝑆 = 𝑆} L) (α ⊔ L) (α ⊔ L)
Sub-Lattice = record { Carrier = Subᴸ
; _≈_ = _≈_
; _≤_ = _≤_
; _∨_ = _∨_
; _∧_ = _∧_
; isLattice = Sub-isLattice
}
```
#### The bounds: empty and full subuniverses
The bottom subuniverse `0ˢ` is the *least* subuniverse, obtained as the one generated
by the empty predicate (`0ˢ = Sg ∅`); its minimality is immediate from `sgIsSmallest`.
The top subuniverse `1ˢ` is the whole carrier, trivially closed under the operations.
```agda
private
0R : Pred A L
0R _ = Lift L ⊥
1R : Pred A L
1R _ = Lift L ⊤
0ˢ : Subᴸ
0ˢ = Sg 𝑨 0R , sgIsSub 𝑨
1ˢ : Subᴸ
1ˢ = 1R , λ _ _ _ → lift tt
0ˢ-minimum : Minimum _≤_ 0ˢ
0ˢ-minimum B = sgIsSmallest 𝑨 (proj₁ B) (proj₂ B) (λ { (lift ()) })
1ˢ-maximum : Maximum _≤_ 1ˢ
1ˢ-maximum B _ = lift tt
Sub-isBoundedLattice : IsBoundedLattice _≈_ _≤_ _∨_ _∧_ 1ˢ 0ˢ
Sub-isBoundedLattice = record { isLattice = Sub-isLattice
; maximum = 1ˢ-maximum
; minimum = 0ˢ-minimum
}
Sub-BoundedLattice : BoundedLattice (α ⊔ ov {𝑆 = 𝑆} L) (α ⊔ L) (α ⊔ L)
Sub-BoundedLattice = record { Carrier = Subᴸ
; _≈_ = _≈_
; _≤_ = _≤_
; _∨_ = _∨_
; _∧_ = _∧_
; ⊤ = 1ˢ
; ⊥ = 0ˢ
; isBoundedLattice = Sub-isBoundedLattice
}
```
#### Infinitary meets and joins
For a family `𝒜 : I → Subᴸ` indexed by `I : Type ℓ₀`, the infinitary meet is the
intersection `⨅ 𝒜` (which holds at `x` iff every `𝒜 i` does), and the infinitary join
is the subuniverse generated by the union, `⨆ 𝒜 = Sg(⋃ 𝒜)`. Both stay at level `L`
because `I` is `ℓ₀`-small.
```agda
⨅ : {I : Type ℓ₀} → (I → Subᴸ) → Subᴸ
⨅ {I} 𝒜 = ⋂ I (λ i → proj₁ (𝒜 i))
, ⋂s {𝑨 = 𝑨} I {𝒜 = λ i → proj₁ (𝒜 i)} (λ i → proj₂ (𝒜 i))
⨆ : {I : Type ℓ₀} → (I → Subᴸ) → Subᴸ
⨆ {I} 𝒜 = Sg 𝑨 (⋃ I (λ i → proj₁ (𝒜 i))) , sgIsSub 𝑨
⨅-lower : {I : Type ℓ₀} (𝒜 : I → Subᴸ) (i : I) → (⨅ 𝒜) ≤ (𝒜 i)
⨅-lower 𝒜 i z = z i
⨅-greatest : {I : Type ℓ₀} (𝒜 : I → Subᴸ) (D : Subᴸ) → (∀ i → D ≤ (𝒜 i)) → D ≤ (⨅ 𝒜)
⨅-greatest 𝒜 D D≤𝒜 z i = D≤𝒜 i z
⨆-upper : {I : Type ℓ₀} (𝒜 : I → Subᴸ) (i : I) → (𝒜 i) ≤ (⨆ 𝒜)
⨆-upper 𝒜 i z = var (i , z)
⨆-least : {I : Type ℓ₀} (𝒜 : I → Subᴸ) (D : Subᴸ) → (∀ i → (𝒜 i) ≤ D) → (⨆ 𝒜) ≤ D
⨆-least 𝒜 D 𝒜≤D = sgIsSmallest 𝑨 (proj₁ D) (proj₂ D) (λ (i , z) → 𝒜≤D i z)
```
#### The complete lattice
`Sub-CompleteLattice`{.AgdaFunction} is the same data extended with the
infinitary meet and join and their four universal properties, presented as the
`CompleteLattice`{.AgdaRecord} record of [Order.CompleteLattice][].
Completeness is where subuniverses are better behaved than subalgebras, and the
asymmetry between the two infinitary operations shows why. An arbitrary
intersection of subuniverses is again a subuniverse, so `⨅`{.AgdaFunction} is the
intersection itself and both `⨅-lower`{.AgdaFunction} and
`⨅-greatest`{.AgdaFunction} are pointwise. A union of subuniverses need not be
one, so `⨆`{.AgdaFunction} has to generate from the union, and its universal
property `⨆-least`{.AgdaFunction} correspondingly goes through
`sgIsSmallest`{.AgdaFunction}.
```agda
Sub-CompleteLattice : CompleteLattice (α ⊔ ov {𝑆 = 𝑆} L) (α ⊔ L) (α ⊔ L) ℓ₀
Sub-CompleteLattice = record
{ Carrier = Subᴸ
; _≈_ = _≈_
; _≤_ = _≤_
; isPartialOrder = ≤-isPartialOrder
; ⨆ = ⨆
; ⨅ = ⨅
; ⨆-upper = ⨆-upper
; ⨆-least = ⨆-least
; ⨅-lower = ⨅-lower
; ⨅-greatest = ⨅-greatest
}
```