From 1d40f953de7bdfbaff350a953c60b2c5951f42a2 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Mon, 27 Apr 2026 15:38:36 -0500 Subject: Add bounded distributive lattices --- Lattice/Bundle/BoundedDistributive.agda | 38 +++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) create mode 100644 Lattice/Bundle/BoundedDistributive.agda (limited to 'Lattice/Bundle') diff --git a/Lattice/Bundle/BoundedDistributive.agda b/Lattice/Bundle/BoundedDistributive.agda new file mode 100644 index 0000000..e2ac964 --- /dev/null +++ b/Lattice/Bundle/BoundedDistributive.agda @@ -0,0 +1,38 @@ +{-# OPTIONS --without-K --safe #-} + +module Lattice.Bundle.BoundedDistributive where + +open import Algebra using (Op₂) +open import Lattice.Structure.IsBoundedDistributive using (IsBoundedDistributiveLattice) +open import Level using (suc; _⊔_) +open import Relation.Binary using (Rel) +open import Relation.Binary.Lattice using (BoundedLattice; DistributiveLattice) + +record BoundedDistributiveLattice c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where + infix 4 _≈_ _≤_ + infixr 6 _∨_ + infixr 7 _∧_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ₁ -- The underlying equality. + _≤_ : Rel Carrier ℓ₂ -- The partial order. + _∨_ : Op₂ Carrier -- The join operation. + _∧_ : Op₂ Carrier -- The meet operation. + ⊤ : Carrier -- The maximum + ⊥ : Carrier -- The minimum + isBoundedDistributiveLattice : IsBoundedDistributiveLattice _≈_ _≤_ _∨_ _∧_ ⊤ ⊥ + + open IsBoundedDistributiveLattice isBoundedDistributiveLattice public + + boundedLattice : BoundedLattice c ℓ₁ ℓ₂ + boundedLattice = record + { isBoundedLattice = isBoundedLattice + } + + distributiveLattice : DistributiveLattice c ℓ₁ ℓ₂ + distributiveLattice = record + { isDistributiveLattice = isDistributiveLattice + } + + open BoundedLattice boundedLattice public + using (lattice; joinSemilattice; meetSemilattice; poset; preorder; setoid) -- cgit v1.2.3