Classical.Structures.Lattice.OrdinalSum¶
Ordinal sums of lattices¶
This is the Classical.Structures.Lattice.OrdinalSum module of the Agda Universal Algebra Library.
The adjoined ordinal sum of lattices 𝓛₁ and 𝓛₂ stacks
𝓛₂ on top of 𝓛₁ and glues the top of 𝓛₁
to the bottom of 𝓛₂: every element of the lower summand lies below
every element of the upper one, and the two chosen extrema become a single element.
This is the operation denoted by L ⊕ₐ M in the small-lattice representations manuscript
(docs/papers/fin-lat-rep/SmallLatticeReps.tex,
§ Ordinal Sums).
The unglued ordinal sum, in which the top of the lower summand is covered by the
bottom of the upper, is the derived composite (𝓛₁ ⊕ₐ chain₂) ⊕ₐ 𝓛₂, gluing a
two-element chain in the middle leaves exactly one covering edge, so the glued form
is the module's single canonical primitive.
Because the sum glues at chosen extrema, the construction takes them as data: a
TopOf 𝓛₁ and a BottomOf 𝓛₂
(Classical.Properties.Lattice).1
Remarks on the design¶
- Gluing is by setoid equality, not element removal.
The carrier is the disjoint union A ⊎ B with the equivalence coarsened so that
inj₁ ⊤₁ ≈ inj₂ ⊥₂; removing a point would require deciding equality with it,
whereas coarsening is constructive and level-polymorphic.
The amalgam setoid is isolated in GlueSetoid, defined for any two
pointed setoids: its equivalence is the pullback of the component equivalences
along the two retractions that collapse the opposite summand to the basepoint.
This pullback presentation makes reflexivity, symmetry, and transitivity componentwise — no case analysis — and on each summand it restricts to the original equivalence, while across summands it holds exactly at the glue.
It is carried by a record indexed by its two endpoints, not by a defined relation; see the section Why a record and not a relation below.2
- The operations never cross the glue.
Meet sends a mixed pair to its lower summand's member and join to its upper one,
so the eight lattice equations hold by case analysis with the component laws on
the diagonal cases and definitional reduction elsewhere; only the congruence of
the operations interacts with the glue, and there the extremum laws (x ∧ ⊤ ≈ x,
⊥ ∨ x ≈ x, and their mirrors) discharge every case.
The first consumer is the FLRP closure toolkit (FLRP.Closure), which represents the ordinal sum as a congruence lattice whenever its summands are so representable.3
The amalgam of two pointed setoids¶
GlueSetoid 𝐴 a₀ 𝐵 b₀ is the disjoint union of the carriers with
inj₁ a₀ and inj₂ b₀ identified. The equivalence is stated through the two
retractions: retractˡ keeps the left summand and collapses the right
to a₀, and retractʳ mirrors it; two elements are equal exactly
when both retractions agree.
On inj₁/inj₁ pairs the right retraction is constantly b₀, so the condition is
the left equivalence (dually on inj₂/inj₂), and on mixed pairs it says precisely
"left component at a₀, right component at b₀."
module GlueSetoid (𝐴 : Setoid α ρ) (a₀ : Setoid.Carrier 𝐴) -- ASSUMPTION: 𝑨 is nonempty (𝐵 : Setoid β σ) (b₀ : Setoid.Carrier 𝐵) -- ASSUMPTION: 𝑩 is nonempty where open Setoid 𝐴 renaming ( Carrier to A ; _≈_ to _≈₁_ ; refl to refl₁ ; sym to sym₁ ; trans to trans₁ ) open Setoid 𝐵 renaming ( Carrier to B ; _≈_ to _≈₂_ ; refl to refl₂ ; sym to sym₂ ; trans to trans₂ ) -- Keep the left summand; collapse the right to the left basepoint. retractˡ : A ⊎ B → A retractˡ (inj₁ x) = x retractˡ (inj₂ _) = a₀ -- Keep the right summand; collapse the left to the right basepoint. retractʳ : A ⊎ B → B retractʳ (inj₁ _) = b₀ retractʳ (inj₂ y) = y -- Glued equality: both retractions agree. A *record* indexed by the two -- endpoints, not a defined relation — see the note below. record _≈ᵍ_ (x y : A ⊎ B) : Type (ρ ⊔ σ) where constructor _∧ᵍ_ field ≈ˡ : retractˡ x ≈₁ retractˡ y ≈ʳ : retractʳ x ≈₂ retractʳ y infix 4 _≈ᵍ_ infixr 4 _∧ᵍ_ open _≈ᵍ_ public open Setoid -- The amalgam setoid: A ⊎ B with the basepoints identified. glueSetoid : Setoid (α ⊔ β) (ρ ⊔ σ) glueSetoid .Carrier = A ⊎ B glueSetoid ._≈_ = _≈ᵍ_ glueSetoid .isEquivalence = record { refl = refl₁ ∧ᵍ refl₂ ; sym = λ (e₁ ∧ᵍ e₂) → sym₁ e₁ ∧ᵍ sym₂ e₂ ; trans = λ (d₁ ∧ᵍ d₂) (e₁ ∧ᵍ e₂) → trans₁ d₁ e₁ ∧ᵍ trans₂ d₂ e₂ } -- The glue itself: the two basepoints are identified. glue-≈ : inj₁ a₀ ≈ᵍ inj₂ b₀ glue-≈ = refl₁ ∧ᵍ refl₂ -- Injections are ≈-embeddings: the intro forms supply the constant component. ≈ᵍ-inj₁ : {x y : A} → x ≈₁ y → inj₁ x ≈ᵍ inj₁ y ≈ᵍ-inj₁ e = e ∧ᵍ refl₂ ≈ᵍ-inj₂ : {x y : B} → x ≈₂ y → inj₂ x ≈ᵍ inj₂ y ≈ᵍ-inj₂ e = refl₁ ∧ᵍ e
The elimination forms are the two fields:
≈ˡof aninj₁/inj₁equation is the left equivalence,≈ʳof aninj₂/inj₂equation the right one,
and on a mixed pair the two fields are exactly the basepoint conditions.
Why a record and not a relation¶
The mathematically obvious phrasing of the same relation is the defined pullback
x ≈ᵍ y = (retractˡ x ≈₁ retractˡ y) × (retractʳ x ≈₂ retractʳ y)
and that phrasing is hostile to Agda's unifier.
A defined relation is unfolded whenever the type checker must infer an implicit endpoint whose type mentions it, leaving constraints whose metavariables sit under the retractions,
retractˡ _x = retractˡ x retractʳ _x = retractʳ x
which are permanently stuck, for two independent reasons.
-
The retractions are genuinely non-injective (each collapses a whole summand to a basepoint), so the constraint cannot be inverted.
-
The carrier
A ⊎ Bis a datatype without an η-rule, so the metavariable cannot be η-expanded into components the way aΣ-typed one can.
The sibling product construction (Classical.Structures.Lattice.Product) defines
its equivalence through proj₁/proj₂, which are just as non-injective — but there
Σ-η lets Agda solve the projected metas componentwise, so inference never breaks.
The failure needs exactly the combination present here: defined relation,
non-injective non-variable head, no η on the carrier.
A one-constructor record indexed by the two endpoints keeps every good property of the pullback presentation:
- reflexivity, symmetry, and transitivity are still componentwise with no case analysis;
- on each summand the fields still reduce to that summand's equivalence, and across summands to the glue condition;
- η keeps proofs pair-like.
Moreover, it makes the relation a record type former, hence injective for unification.
A constraint ?x ≈ᵍ ?y ≟ a ≈ᵍ b now solves the endpoints before any retraction is
exposed, so implicit-endpoint lemmas (Setoid.refl/sym/trans at ≈ᵍ,
congruences passed under-applied to record-constructor arguments,
parameterized-module applications) all infer. The "canary" below fails to type-check
the moment that property is lost.4
The idiom generalizes: any relation defined by restriction along a non-injective map — including relations built downstream through these same retractions — should be a record indexed by its endpoints rather than a definition.
-- Canary: an implicit endpoint under `_≈ᵍ_` must be inferable. This fails -- with [UnsolvedMetaVariables] if `_≈ᵍ_` ever reverts to a defined relation. _ : ∀ x → x ≈ᵍ x _ = λ x → Setoid.refl glueSetoid
The ordinal-sum construction¶
LatticeOrdinalSum packages the development for fixed summands and
extremum choices; opening it provides the glued carrier, the operations with
their congruences and equations, the sum lattice, and the characterization of its
order.
In this module we adopt the following notational convention: for i ∈ {1, 2},
𝓛ᵢdenotes a full lattice structure: carrier, operations, and lattice laws;𝑳ᵢdenotes the carrier and operations of the lattice𝓛ᵢ;Lᵢdenotes just the carrier of𝓛ᵢ.
module LatticeOrdinalSum (𝓛₁ : Lattice α ρ) ((⊤₁ , ⊤₁max) : TopOf 𝓛₁) -- ASSUMPTION: 𝓛₁ has maximal element ⊤₁ (𝓛₂ : Lattice β σ) ((⊥₂ , ⊥₂min) : BottomOf 𝓛₂) -- ASSUMPTION: 𝓛₂ has minimal element ⊥₂ where private 𝑳₁ : Algebra {𝑆 = Sig-Lattice} α ρ 𝑳₁ = proj₁ 𝓛₁ 𝑳₂ : Algebra {𝑆 = Sig-Lattice} β σ 𝑳₂ = proj₁ 𝓛₂ L₁ : Type α L₁ = 𝕌[ 𝑳₁ ] L₂ : Type β L₂ = 𝕌[ 𝑳₂ ] 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ʳ₂ ) open Lattice-Order 𝓛₁ using () renaming ( _≤_ to _≤₁_ ; ≤-via-∨ to ≤-via-∨₁ ) open Lattice-Order 𝓛₂ using () renaming ( _≤_ to _≤₂_ ; ≤-via-∨ to ≤-via-∨₂ )
The absorption behaviour of the chosen extrema, in the eight one-sided forms the
case analyses below consume. Note that x ≤₁ ⊤₁ is x ∧₁ ⊤₁ ≈₁ x and
⊥₂ ≤₂ x is ⊥₂ ∧₂ x ≈₂ ⊥₂, definitionally, so half of these are the
universal properties themselves.
private x∧⊤ : ∀ x → x ∧₁ ⊤₁ ≈₁ x x∧⊤ x = ⊤₁max x ⊤∧x : ∀ x → ⊤₁ ∧₁ x ≈₁ x ⊤∧x x = trans₁ ∧₁-comm (x∧⊤ x) x∨⊤ : ∀ x → x ∨₁ ⊤₁ ≈₁ ⊤₁ x∨⊤ x = ≤-via-∨₁ (⊤₁max x) ⊤∨x : ∀ x → ⊤₁ ∨₁ x ≈₁ ⊤₁ ⊤∨x x = trans₁ ∨₁-comm (x∨⊤ x) ⊥∧x : ∀ x → ⊥₂ ∧₂ x ≈₂ ⊥₂ ⊥∧x x = ⊥₂min x x∧⊥ : ∀ x → x ∧₂ ⊥₂ ≈₂ ⊥₂ x∧⊥ x = trans₂ ∧₂-comm (⊥∧x x) ⊥∨x : ∀ x → ⊥₂ ∨₂ x ≈₂ x ⊥∨x x = ≤-via-∨₂ (⊥₂min x) x∨⊥ : ∀ x → x ∨₂ ⊥₂ ≈₂ x x∨⊥ x = trans₂ ∨₂-comm (⊥∨x x)
The glued carrier at the two chosen extrema.
open GlueSetoid 𝔻[ 𝑳₁ ] ⊤₁ 𝔻[ 𝑳₂ ] ⊥₂ public private A⊎B : Type (α ⊔ β) A⊎B = L₁ ⊎ L₂
Meet and join.
A mixed meet lands in the lower summand and a mixed join in the upper one — the lower summand lies entirely below the upper.
_∧ᵒ_ : A⊎B → A⊎B → A⊎B inj₁ x ∧ᵒ inj₁ y = inj₁ (x ∧₁ y) inj₁ x ∧ᵒ inj₂ y = inj₁ x inj₂ x ∧ᵒ inj₁ y = inj₁ y inj₂ x ∧ᵒ inj₂ y = inj₂ (x ∧₂ y) _∨ᵒ_ : A⊎B → A⊎B → A⊎B inj₁ x ∨ᵒ inj₁ y = inj₁ (x ∨₁ y) inj₁ x ∨ᵒ inj₂ y = inj₂ y inj₂ x ∨ᵒ inj₁ y = inj₂ x inj₂ x ∨ᵒ inj₂ y = inj₂ (x ∨₂ y) infixr 7 _∧ᵒ_ infixr 6 _∨ᵒ_
Congruence.
This is the one place the glue matters. Each of the sixteen constructor combinations
reduces to a pair of component goals; the diagonal combinations are the component
congruences, and every combination that crosses the glue is discharged by the
extremum-absorption lemmas above (an argument ≈ᵍ-related across the glue pins its
left component to ⊤₁ or its right one to ⊥₂, and absorption then collapses the
affected meet or join).
∧ᵒ-cong : ∀ {p q u v} → p ≈ᵍ q → u ≈ᵍ v → p ∧ᵒ u ≈ᵍ q ∧ᵒ v
∨ᵒ-cong : ∀ {p q u v} → p ≈ᵍ q → u ≈ᵍ v → p ∨ᵒ u ≈ᵍ q ∨ᵒ v
The eight equations.
The operations never cross the glue, so every mixed case reduces definitionally and
is closed by reflexivity; the diagonal cases are the component laws, and the two
absorption laws additionally consume one idempotency step in their
inj₂-meets-inj₁ (resp. mirrored) case.
∧ᵒ-assoc : ∀ {p q r} → (p ∧ᵒ q) ∧ᵒ r ≈ᵍ p ∧ᵒ (q ∧ᵒ r) ∧ᵒ-assoc {inj₁ _} {inj₁ _} {inj₁ _} = ∧₁-assoc ∧ᵍ refl₂ ∧ᵒ-assoc {inj₂ _} {inj₂ _} {inj₂ _} = refl₁ ∧ᵍ ∧₂-assoc ∧ᵒ-assoc {inj₁ _} {inj₁ _} {inj₂ _} = refl₁ ∧ᵍ refl₂ ∧ᵒ-assoc {inj₁ _} {inj₂ _} {inj₁ _} = refl₁ ∧ᵍ refl₂ ∧ᵒ-assoc {inj₂ _} {inj₁ _} {inj₁ _} = refl₁ ∧ᵍ refl₂ ∧ᵒ-assoc {inj₁ _} {inj₂ _} {inj₂ _} = refl₁ ∧ᵍ refl₂ ∧ᵒ-assoc {inj₂ _} {inj₁ _} {inj₂ _} = refl₁ ∧ᵍ refl₂ ∧ᵒ-assoc {inj₂ _} {inj₂ _} {inj₁ _} = refl₁ ∧ᵍ refl₂ ∧ᵒ-comm : ∀ {p q} → p ∧ᵒ q ≈ᵍ q ∧ᵒ p ∧ᵒ-comm {inj₁ _} {inj₁ _} = ∧₁-comm ∧ᵍ refl₂ ∧ᵒ-comm {inj₁ _} {inj₂ _} = refl₁ ∧ᵍ refl₂ ∧ᵒ-comm {inj₂ _} {inj₁ _} = refl₁ ∧ᵍ refl₂ ∧ᵒ-comm {inj₂ _} {inj₂ _} = refl₁ ∧ᵍ ∧₂-comm ∧ᵒ-idem : ∀ {p} → p ∧ᵒ p ≈ᵍ p ∧ᵒ-idem {inj₁ _} = ∧₁-idem ∧ᵍ refl₂ ∧ᵒ-idem {inj₂ _} = refl₁ ∧ᵍ ∧₂-idem ∨ᵒ-assoc : ∀ {p q r} → (p ∨ᵒ q) ∨ᵒ r ≈ᵍ p ∨ᵒ (q ∨ᵒ r) ∨ᵒ-assoc {inj₁ _} {inj₁ _} {inj₁ _} = ∨₁-assoc ∧ᵍ refl₂ ∨ᵒ-assoc {inj₂ _} {inj₂ _} {inj₂ _} = refl₁ ∧ᵍ ∨₂-assoc ∨ᵒ-assoc {inj₁ _} {inj₁ _} {inj₂ _} = refl₁ ∧ᵍ refl₂ ∨ᵒ-assoc {inj₁ _} {inj₂ _} {inj₁ _} = refl₁ ∧ᵍ refl₂ ∨ᵒ-assoc {inj₁ _} {inj₂ _} {inj₂ _} = refl₁ ∧ᵍ refl₂ ∨ᵒ-assoc {inj₂ _} {inj₁ _} {inj₁ _} = refl₁ ∧ᵍ refl₂ ∨ᵒ-assoc {inj₂ _} {inj₁ _} {inj₂ _} = refl₁ ∧ᵍ refl₂ ∨ᵒ-assoc {inj₂ _} {inj₂ _} {inj₁ _} = refl₁ ∧ᵍ refl₂ ∨ᵒ-comm : ∀ {p q} → p ∨ᵒ q ≈ᵍ q ∨ᵒ p ∨ᵒ-comm {inj₁ _} {inj₁ _} = ∨₁-comm ∧ᵍ refl₂ ∨ᵒ-comm {inj₁ _} {inj₂ _} = refl₁ ∧ᵍ refl₂ ∨ᵒ-comm {inj₂ _} {inj₁ _} = refl₁ ∧ᵍ refl₂ ∨ᵒ-comm {inj₂ _} {inj₂ _} = refl₁ ∧ᵍ ∨₂-comm ∨ᵒ-idem : ∀ {p} → p ∨ᵒ p ≈ᵍ p ∨ᵒ-idem {inj₁ _} = ∨₁-idem ∧ᵍ refl₂ ∨ᵒ-idem {inj₂ _} = refl₁ ∧ᵍ ∨₂-idem absorbˡᵒ : ∀ {p q} → p ∧ᵒ (p ∨ᵒ q) ≈ᵍ p absorbˡᵒ {inj₁ _} {inj₁ _} = absorbˡ₁ ∧ᵍ refl₂ absorbˡᵒ {inj₁ _} {inj₂ _} = refl₁ ∧ᵍ refl₂ absorbˡᵒ {inj₂ _} {inj₁ _} = refl₁ ∧ᵍ ∧₂-idem absorbˡᵒ {inj₂ _} {inj₂ _} = refl₁ ∧ᵍ absorbˡ₂ absorbʳᵒ : ∀ {p q} → (p ∧ᵒ q) ∨ᵒ p ≈ᵍ p absorbʳᵒ {inj₁ _} {inj₁ _} = absorbʳ₁ ∧ᵍ refl₂ absorbʳᵒ {inj₁ _} {inj₂ _} = ∨₁-idem ∧ᵍ refl₂ absorbʳᵒ {inj₂ _} {inj₁ _} = refl₁ ∧ᵍ refl₂ absorbʳᵒ {inj₂ _} {inj₂ _} = refl₁ ∧ᵍ absorbʳ₂
Assembling through the setoid-level builder yields the ordinal sum. Every
argument is passed under-applied: the record presentation of _≈ᵍ_
lets Agda recover each implicit endpoint from the expected type, so none of them
has to be forwarded by hand.
⊕-Lattice : Lattice (α ⊔ β) (ρ ⊔ σ) ⊕-Lattice = setoidEqsToLattice glueSetoid _∧ᵒ_ _∨ᵒ_ ∧ᵒ-cong ∨ᵒ-cong ∧ᵒ-assoc ∧ᵒ-comm ∧ᵒ-idem ∨ᵒ-assoc ∨ᵒ-comm ∨ᵒ-idem absorbˡᵒ absorbʳᵒ
The sum order, characterized.
The meet order of the sum unfolds definitionally on each constructor combination: within a summand it is that summand's order, everything low is below everything high, and the only way an upper element sits below a lower one is at the glue. The four lemmas name these unfoldings for consumers.
open Lattice-Order ⊕-Lattice using () renaming ( _≤_ to _≤ᵒ_ ) -- Within the lower summand, the sum order is the lower order. ≤ᵒ-inj₁ : {x y : L₁} → x ≤₁ y → inj₁ x ≤ᵒ inj₁ y ≤ᵒ-inj₁ e = e ∧ᵍ refl₂ ≤ᵒ-inj₁-elim : {x y : L₁} → inj₁ x ≤ᵒ inj₁ y → x ≤₁ y ≤ᵒ-inj₁-elim = ≈ˡ -- Within the upper summand, the sum order is the upper order. ≤ᵒ-inj₂ : {x y : L₂} → x ≤₂ y → inj₂ x ≤ᵒ inj₂ y ≤ᵒ-inj₂ e = refl₁ ∧ᵍ e ≤ᵒ-inj₂-elim : {x y : L₂} → inj₂ x ≤ᵒ inj₂ y → x ≤₂ y ≤ᵒ-inj₂-elim = ≈ʳ -- Everything in the lower summand is below everything in the upper one. ≤ᵒ-up : {x : L₁} {y : L₂} → inj₁ x ≤ᵒ inj₂ y ≤ᵒ-up = refl₁ ∧ᵍ refl₂ -- An upper element below a lower one forces both to the glue ... ≤ᵒ-down-elim : {x : L₂} {y : L₁} → inj₂ x ≤ᵒ (inj₁ y) → (y ≈₁ ⊤₁) × (x ≈₂ ⊥₂) ≤ᵒ-down-elim (p ∧ᵍ q) = p , sym₂ q -- ... and, at the glue, it does sit below. ≤ᵒ-down : {x : L₂} {y : L₁} → y ≈₁ ⊤₁ → x ≈₂ ⊥₂ → inj₂ x ≤ᵒ inj₁ y ≤ᵒ-down y≈⊤ x≈⊥ = y≈⊤ ∧ᵍ sym₂ x≈⊥
The sum operator.
The standalone operator, for consumers who need only the lattice.
ordinalSum : (𝓛₁ : Lattice α ρ) → TopOf 𝓛₁ → (𝓛₂ : Lattice β σ) → BottomOf 𝓛₂ → Lattice (α ⊔ β) (ρ ⊔ σ) ordinalSum 𝓛₁ t 𝓛₂ b = LatticeOrdinalSum.⊕-Lattice 𝓛₁ t 𝓛₂ b
-
General lattices need not have extrema, and threading the choice keeps the construction total and the resulting carrier syntactically predictable (the corollaries that adjoin a fresh extremum to a lattice instantiate a summand at
chain₂and its concrete0/1). ↩ -
The same idiom should be applied to any relation built by restriction along a non-injective map. ↩
-
See Work Package 5 (WP-5) of the roadmap. ↩
-
The full failure analysis, the minimal reproduction, and the rejected alternatives (a four-constructor inductive family, an
opaqueblock, an injectivity pragma) are in Issue #504. ↩