blob: dfd67d892a4fd2e29f9a8ab6159a733d1fad1474 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
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ˡ-∨
}
|
