Skip to content

Commit b449551

Browse files
laMudriMatthewDaggitt
laMudri
authored and
MatthewDaggitt
committed
[ refactor ] create Algebra.Lattice hierarchy
1 parent 516c545 commit b449551

File tree

5 files changed

+384
-209
lines changed

5 files changed

+384
-209
lines changed

‎src/Algebra/Bundles.agda

Lines changed: 0 additions & 119 deletions
Original file line numberDiff line numberDiff line change
@@ -143,25 +143,6 @@ record CommutativeSemigroup c ℓ : Set (suc (c ⊔ ℓ)) where
143143
commutativeMagma : CommutativeMagma c ℓ
144144
commutativeMagma = record { isCommutativeMagma = isCommutativeMagma }
145145

146-
147-
record Semilattice c ℓ : Set (suc (c ⊔ ℓ)) where
148-
infixr 7 _∧_
149-
infix 4 _≈_
150-
field
151-
Carrier : Set c
152-
_≈_ : Rel Carrier ℓ
153-
_∧_ : Op₂ Carrier
154-
isSemilattice : IsSemilattice _≈_ _∧_
155-
156-
open IsSemilattice isSemilattice public
157-
158-
band : Band c ℓ
159-
band = record { isBand = isBand }
160-
161-
open Band band public
162-
using (_≉_; rawMagma; magma; semigroup)
163-
164-
165146
------------------------------------------------------------------------
166147
-- Bundles with 1 binary operation & 1 element
167148
------------------------------------------------------------------------
@@ -393,81 +374,6 @@ record AbelianGroup c ℓ : Set (suc (c ⊔ ℓ)) where
393374
open CommutativeMonoid commutativeMonoid public
394375
using (commutativeMagma; commutativeSemigroup)
395376

396-
397-
------------------------------------------------------------------------
398-
-- Bundles with 2 binary operations
399-
------------------------------------------------------------------------
400-
401-
record RawLattice c ℓ : Set (suc (c ⊔ ℓ)) where
402-
infixr 7 _∧_
403-
infixr 6 _∨_
404-
infix 4 _≈_
405-
field
406-
Carrier : Set c
407-
_≈_ : Rel Carrier ℓ
408-
_∧_ : Op₂ Carrier
409-
_∨_ : Op₂ Carrier
410-
411-
∨-rawMagma : RawMagma c ℓ
412-
∨-rawMagma = record { _≈_ = _≈_; _∙_ = _∨_ }
413-
414-
∧-rawMagma : RawMagma c ℓ
415-
∧-rawMagma = record { _≈_ = _≈_; _∙_ = _∧_ }
416-
417-
open RawMagma ∨-rawMagma public
418-
using (_≉_)
419-
420-
421-
record Lattice c ℓ : Set (suc (c ⊔ ℓ)) where
422-
infixr 7 _∧_
423-
infixr 6 _∨_
424-
infix 4 _≈_
425-
field
426-
Carrier : Set c
427-
_≈_ : Rel Carrier ℓ
428-
_∨_ : Op₂ Carrier
429-
_∧_ : Op₂ Carrier
430-
isLattice : IsLattice _≈_ _∨_ _∧_
431-
432-
open IsLattice isLattice public
433-
434-
rawLattice : RawLattice c ℓ
435-
rawLattice = record
436-
{ _≈_ = _≈_
437-
; _∧_ = _∧_
438-
; _∨_ = _∨_
439-
}
440-
441-
open RawLattice rawLattice public
442-
using (∨-rawMagma; ∧-rawMagma)
443-
444-
setoid : Setoid _ _
445-
setoid = record { isEquivalence = isEquivalence }
446-
447-
open Setoid setoid public
448-
using (_≉_)
449-
450-
451-
record DistributiveLattice c ℓ : Set (suc (c ⊔ ℓ)) where
452-
infixr 7 _∧_
453-
infixr 6 _∨_
454-
infix 4 _≈_
455-
field
456-
Carrier : Set c
457-
_≈_ : Rel Carrier ℓ
458-
_∨_ : Op₂ Carrier
459-
_∧_ : Op₂ Carrier
460-
isDistributiveLattice : IsDistributiveLattice _≈_ _∨_ _∧_
461-
462-
open IsDistributiveLattice isDistributiveLattice public
463-
464-
lattice : Lattice _ _
465-
lattice = record { isLattice = isLattice }
466-
467-
open Lattice lattice public
468-
using (_≉_; rawLattice; setoid)
469-
470-
471377
------------------------------------------------------------------------
472378
-- Bundles with 2 binary operations & 1 element
473379
------------------------------------------------------------------------
@@ -952,31 +858,6 @@ record CommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where
952858
; commutativeSemiringWithoutOne
953859
)
954860

955-
956-
record BooleanAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where
957-
infix 8 ¬_
958-
infixr 7 _∧_
959-
infixr 6 _∨_
960-
infix 4 _≈_
961-
field
962-
Carrier : Set c
963-
_≈_ : Rel Carrier ℓ
964-
_∨_ : Op₂ Carrier
965-
_∧_ : Op₂ Carrier
966-
¬_ : Op₁ Carrier
967-
⊤ : Carrier
968-
⊥ : Carrier
969-
isBooleanAlgebra : IsBooleanAlgebra _≈_ _∨_ _∧_ ¬_ ⊤ ⊥
970-
971-
open IsBooleanAlgebra isBooleanAlgebra public
972-
973-
distributiveLattice : DistributiveLattice _ _
974-
distributiveLattice = record { isDistributiveLattice = isDistributiveLattice }
975-
976-
open DistributiveLattice distributiveLattice public
977-
using (_≉_; setoid; lattice)
978-
979-
980861
------------------------------------------------------------------------
981862
-- DEPRECATED NAMES
982863
------------------------------------------------------------------------

‎src/Algebra/Lattice.agda

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Definitions of algebraic structures like semilattices and lattices
5+
-- (packed in records together with sets, operations, etc.), defined via
6+
-- meet/join operations and their properties
7+
--
8+
-- For lattices defined via an order relation, see
9+
-- Relation.Binary.Lattice.
10+
------------------------------------------------------------------------
11+
12+
{-# OPTIONS --without-K --safe #-}
13+
14+
module Algebra.Lattice where
15+
16+
open import Algebra.Lattice.Structures public
17+
open import Algebra.Lattice.Bundles public

‎src/Algebra/Lattice/Bundles.agda

Lines changed: 227 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,227 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Definitions of algebraic structures like semilattices and lattices
5+
-- (packed in records together with sets, operations, etc.), defined via
6+
-- meet/join operations and their properties
7+
--
8+
-- For lattices defined via an order relation, see
9+
-- Relation.Binary.Lattice.
10+
------------------------------------------------------------------------
11+
12+
-- The contents of this module should be accessed via `Algebra.Lattice`.
13+
14+
{-# OPTIONS --without-K --safe #-}
15+
16+
module Algebra.Lattice.Bundles where
17+
18+
open import Algebra.Core
19+
open import Algebra.Bundles
20+
open import Algebra.Structures
21+
open import Algebra.Lattice.Structures
22+
open import Relation.Binary
23+
open import Function.Base
24+
open import Level
25+
26+
record Semilattice c ℓ : Set (suc (c ⊔ ℓ)) where
27+
infixr 7 _∙_
28+
infix 4 _≈_
29+
field
30+
Carrier : Set c
31+
_≈_ : Rel Carrier ℓ
32+
_∙_ : Op₂ Carrier
33+
isSemilattice : IsSemilattice _≈_ _∙_
34+
35+
open IsSemilattice isSemilattice public
36+
37+
band : Band c ℓ
38+
band = record { isBand = isBand }
39+
40+
open Band band public
41+
using (_≉_; rawMagma; magma; isMagma; semigroup; isSemigroup; isBand)
42+
43+
44+
record MeetSemilattice c ℓ : Set (suc (c ⊔ ℓ)) where
45+
infixr 7 _∧_
46+
infix 4 _≈_
47+
field
48+
Carrier : Set c
49+
_≈_ : Rel Carrier ℓ
50+
_∧_ : Op₂ Carrier
51+
isMeetSemilattice : IsSemilattice _≈_ _∧_
52+
53+
open IsMeetSemilattice _≈_ isMeetSemilattice public
54+
55+
semilattice : Semilattice c ℓ
56+
semilattice = record { isSemilattice = isMeetSemilattice }
57+
58+
open Semilattice semilattice public
59+
using (rawMagma; magma; semigroup; band)
60+
61+
62+
record JoinSemilattice c ℓ : Set (suc (c ⊔ ℓ)) where
63+
infixr 7 _∨_
64+
infix 4 _≈_
65+
field
66+
Carrier : Set c
67+
_≈_ : Rel Carrier ℓ
68+
_∨_ : Op₂ Carrier
69+
isJoinSemilattice : IsSemilattice _≈_ _∨_
70+
71+
open IsJoinSemilattice _≈_ isJoinSemilattice public
72+
73+
semilattice : Semilattice c ℓ
74+
semilattice = record { isSemilattice = isJoinSemilattice }
75+
76+
open Semilattice semilattice public
77+
using (rawMagma; magma; semigroup; band)
78+
79+
80+
record BoundedSemilattice c ℓ : Set (suc (c ⊔ ℓ)) where
81+
infixr 7 _∙_
82+
infix 4 _≈_
83+
field
84+
Carrier : Set c
85+
_≈_ : Rel Carrier ℓ
86+
_∙_ : Op₂ Carrier
87+
ε : Carrier
88+
isBoundedSemilattice : IsBoundedSemilattice _≈_ _∙_ ε
89+
90+
open IsBoundedSemilattice _≈_ isBoundedSemilattice public
91+
92+
semilattice : Semilattice c ℓ
93+
semilattice = record { isSemilattice = isSemilattice }
94+
95+
open Semilattice semilattice public using (rawMagma; magma; semigroup; band)
96+
97+
record BoundedMeetSemilattice c ℓ : Set (suc (c ⊔ ℓ)) where
98+
infixr 7 _∧_
99+
infix 4 _≈_
100+
field
101+
Carrier : Set c
102+
_≈_ : Rel Carrier ℓ
103+
_∧_ : Op₂ Carrier
104+
⊤ : Carrier
105+
isBoundedMeetSemilattice : IsBoundedSemilattice _≈_ _∧_ ⊤
106+
107+
open IsBoundedMeetSemilattice _≈_ isBoundedMeetSemilattice public
108+
109+
boundedSemilattice : BoundedSemilattice c ℓ
110+
boundedSemilattice = record
111+
{ isBoundedSemilattice = isBoundedMeetSemilattice }
112+
113+
open BoundedSemilattice boundedSemilattice public
114+
using (rawMagma; magma; semigroup; band; semilattice)
115+
116+
117+
record BoundedJoinSemilattice c ℓ : Set (suc (c ⊔ ℓ)) where
118+
infixr 7 _∨_
119+
infix 4 _≈_
120+
field
121+
Carrier : Set c
122+
_≈_ : Rel Carrier ℓ
123+
_∨_ : Op₂ Carrier
124+
⊥ : Carrier
125+
isBoundedJoinSemilattice : IsBoundedSemilattice _≈_ _∨_ ⊥
126+
127+
open IsBoundedJoinSemilattice _≈_ isBoundedJoinSemilattice public
128+
129+
boundedSemilattice : BoundedSemilattice c ℓ
130+
boundedSemilattice = record
131+
{ isBoundedSemilattice = isBoundedJoinSemilattice }
132+
133+
open BoundedSemilattice boundedSemilattice public
134+
using (rawMagma; magma; semigroup; band; semilattice)
135+
136+
record RawLattice c ℓ : Set (suc (c ⊔ ℓ)) where
137+
infixr 7 _∧_
138+
infixr 6 _∨_
139+
infix 4 _≈_
140+
field
141+
Carrier : Set c
142+
_≈_ : Rel Carrier ℓ
143+
_∧_ : Op₂ Carrier
144+
_∨_ : Op₂ Carrier
145+
146+
∨-rawMagma : RawMagma c ℓ
147+
∨-rawMagma = record { _≈_ = _≈_; _∙_ = _∨_ }
148+
149+
∧-rawMagma : RawMagma c ℓ
150+
∧-rawMagma = record { _≈_ = _≈_; _∙_ = _∧_ }
151+
152+
open RawMagma ∨-rawMagma public
153+
using (_≉_)
154+
155+
156+
record Lattice c ℓ : Set (suc (c ⊔ ℓ)) where
157+
infixr 7 _∧_
158+
infixr 6 _∨_
159+
infix 4 _≈_
160+
field
161+
Carrier : Set c
162+
_≈_ : Rel Carrier ℓ
163+
_∨_ : Op₂ Carrier
164+
_∧_ : Op₂ Carrier
165+
isLattice : IsLattice _≈_ _∨_ _∧_
166+
167+
open IsLattice isLattice public
168+
169+
rawLattice : RawLattice c ℓ
170+
rawLattice = record
171+
{ _≈_ = _≈_
172+
; _∧_ = _∧_
173+
; _∨_ = _∨_
174+
}
175+
176+
open RawLattice rawLattice public
177+
using (∨-rawMagma; ∧-rawMagma)
178+
179+
setoid : Setoid _ _
180+
setoid = record { isEquivalence = isEquivalence }
181+
182+
open Setoid setoid public
183+
using (_≉_)
184+
185+
186+
record DistributiveLattice c ℓ : Set (suc (c ⊔ ℓ)) where
187+
infixr 7 _∧_
188+
infixr 6 _∨_
189+
infix 4 _≈_
190+
field
191+
Carrier : Set c
192+
_≈_ : Rel Carrier ℓ
193+
_∨_ : Op₂ Carrier
194+
_∧_ : Op₂ Carrier
195+
isDistributiveLattice : IsDistributiveLattice _≈_ _∨_ _∧_
196+
197+
open IsDistributiveLattice isDistributiveLattice public
198+
199+
lattice : Lattice _ _
200+
lattice = record { isLattice = isLattice }
201+
202+
open Lattice lattice public
203+
using (_≉_; rawLattice; setoid)
204+
205+
206+
record BooleanAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where
207+
infix 8 ¬_
208+
infixr 7 _∧_
209+
infixr 6 _∨_
210+
infix 4 _≈_
211+
field
212+
Carrier : Set c
213+
_≈_ : Rel Carrier ℓ
214+
_∨_ : Op₂ Carrier
215+
_∧_ : Op₂ Carrier
216+
¬_ : Op₁ Carrier
217+
⊤ : Carrier
218+
⊥ : Carrier
219+
isBooleanAlgebra : IsBooleanAlgebra _≈_ _∨_ _∧_ ¬_ ⊤ ⊥
220+
221+
open IsBooleanAlgebra isBooleanAlgebra public
222+
223+
distributiveLattice : DistributiveLattice _ _
224+
distributiveLattice = record { isDistributiveLattice = isDistributiveLattice }
225+
226+
open DistributiveLattice distributiveLattice public
227+
using (_≉_; setoid; lattice)

0 commit comments

Comments
 (0)