Add bounded distributive latticesmain

1 files changed, 38 insertions, 0 deletions

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)