blob: bb9f4a23486a94b2ffd57580f3e7bf610817ff63 (
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
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
|
{-# OPTIONS --without-K --safe #-}
module Lattice.Bundle.BoundedDistributive where
import Relation.Binary.Lattice.Properties.BoundedJoinSemilattice as BJS
import Relation.Binary.Lattice.Properties.BoundedLattice as BL
import Relation.Binary.Lattice.Properties.BoundedMeetSemilattice as BMS
import Relation.Binary.Lattice.Properties.DistributiveLattice as DL
import Relation.Binary.Lattice.Properties.JoinSemilattice as JS
import Relation.Binary.Lattice.Properties.MeetSemilattice as MS
open import Algebra using (Op₂)
open import Algebra.Bundles using (Semiring)
open import Data.Product using (_,_)
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; boundedJoinSemilattice; boundedMeetSemilattice; joinSemilattice; meetSemilattice; poset; preorder; setoid)
semiring : Semiring c ℓ₁
semiring = record
{ Carrier = Carrier
; _≈_ = _≈_
; _+_ = _∨_
; _*_ = _∧_
; 0# = ⊥
; 1# = ⊤
; isSemiring = record
{ isSemiringWithoutAnnihilatingZero = record
{ +-isCommutativeMonoid = record
{ isMonoid = record
{ isSemigroup = record
{ isMagma = record
{ isEquivalence = isEquivalence
; ∙-cong = ∨-cong
}
; assoc = ∨-assoc
}
; identity = ∨-identity
}
; comm = ∨-comm
}
; *-cong = ∧-cong
; *-assoc = ∧-assoc
; *-identity = ∧-identity
; distrib = ∧-distribˡ-∨ , ∧-distribʳ-∨
}
; zero = ∧-zero
}
}
where
open BJS boundedJoinSemilattice using () renaming (identity to ∨-identity)
open BL boundedLattice using (∧-zero)
open BMS boundedMeetSemilattice using () renaming (identity to ∧-identity)
open DL distributiveLattice using (∧-distribʳ-∨)
open JS joinSemilattice using (∨-comm; ∨-cong; ∨-assoc)
open MS meetSemilattice using (∧-comm; ∧-cong; ∧-assoc)
|
