From 1d40f953de7bdfbaff350a953c60b2c5951f42a2 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Mon, 27 Apr 2026 15:38:36 -0500
Subject: Add bounded distributive lattices

---
 Lattice/Bundle/BoundedDistributive.agda      | 38 ++++++++++++++++++++++++
 Lattice/Structure/IsBoundedDistributive.agda | 43 ++++++++++++++++++++++++++++
 2 files changed, 81 insertions(+)
 create mode 100644 Lattice/Bundle/BoundedDistributive.agda
 create mode 100644 Lattice/Structure/IsBoundedDistributive.agda

(limited to 'Lattice')

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)
diff --git a/Lattice/Structure/IsBoundedDistributive.agda b/Lattice/Structure/IsBoundedDistributive.agda
new file mode 100644
index 0000000..dfd67d8
--- /dev/null
+++ b/Lattice/Structure/IsBoundedDistributive.agda
@@ -0,0 +1,43 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary using (Rel)
+
+module Lattice.Structure.IsBoundedDistributive
+   {a ℓ₁ ℓ₂} {A : Set a}
+   (_≈_ : Rel A ℓ₁) -- The underlying equality.
+   (_≤_ : Rel A ℓ₂) -- The partial order.
+  where
+
+open import Algebra using (Op₂)
+open import Algebra.Definitions using (_DistributesOverˡ_)
+open import Level using (suc; _⊔_)
+open import Relation.Binary.Definitions using (Minimum; Maximum)
+open import Relation.Binary.Lattice.Structures _≈_ _≤_ using (IsLattice; IsDistributiveLattice; IsBoundedLattice)
+
+record IsBoundedDistributiveLattice
+    (_∨_ : Op₂ A)    -- The join operation.
+    (_∧_ : Op₂ A)    -- The meet operation.
+    (⊤   : A)        -- The maximum.
+    (⊥   : A)        -- The minimum.
+  : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+
+  field
+    isLattice     : IsLattice _∨_ _∧_
+    maximum       : Maximum _≤_ ⊤
+    minimum       : Minimum _≤_ ⊥
+    ∧-distribˡ-∨  : _DistributesOverˡ_ _≈_ _∧_ _∨_
+
+  open IsLattice isLattice public
+
+  isBoundedLattice : IsBoundedLattice _∨_ _∧_ ⊤ ⊥
+  isBoundedLattice = record
+      { isLattice = isLattice
+      ; maximum = maximum
+      ; minimum = minimum
+      }
+
+  isDistributiveLattice : IsDistributiveLattice _∨_ _∧_
+  isDistributiveLattice = record
+      { isLattice = isLattice
+      ; ∧-distribˡ-∨ = ∧-distribˡ-∨
+      }
-- 
cgit v1.2.3