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/Structure/IsBoundedDistributive.agda | 43 ++++++++++++++++++++++++++++
 1 file changed, 43 insertions(+)
 create mode 100644 Lattice/Structure/IsBoundedDistributive.agda

(limited to 'Lattice/Structure/IsBoundedDistributive.agda')

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