Skip to content

Commit 5fa4cd7

Browse files
laMudrilaMudri
committed
[ refactor ] create Algebra.Lattice hierarchy
1 parent 14025c1 commit 5fa4cd7

File tree

5 files changed

+309
-168
lines changed

5 files changed

+309
-168
lines changed

‎src/Algebra/Bundles.agda

Lines changed: 0 additions & 82 deletions
Original file line numberDiff line numberDiff line change
@@ -96,23 +96,6 @@ record CommutativeSemigroup c ℓ : Set (suc (c ⊔ ℓ)) where
9696
open Semigroup semigroup public using (magma; rawMagma)
9797

9898

99-
record Semilattice c ℓ : Set (suc (c ⊔ ℓ)) where
100-
infixr 7 _∧_
101-
infix 4 _≈_
102-
field
103-
Carrier : Set c
104-
_≈_ : Rel Carrier ℓ
105-
_∧_ : Op₂ Carrier
106-
isSemilattice : IsSemilattice _≈_ _∧_
107-
108-
open IsSemilattice isSemilattice public
109-
110-
band : Band c ℓ
111-
band = record { isBand = isBand }
112-
113-
open Band band public using (rawMagma; magma; semigroup)
114-
115-
11699
record SelectiveMagma c ℓ : Set (suc (c ⊔ ℓ)) where
117100
infixl 7 _∙_
118101
infix 4 _≈_
@@ -291,47 +274,6 @@ record AbelianGroup c ℓ : Set (suc (c ⊔ ℓ)) where
291274
commutativeMonoid =
292275
record { isCommutativeMonoid = isCommutativeMonoid }
293276

294-
295-
------------------------------------------------------------------------
296-
-- Bundles with 2 binary operations
297-
------------------------------------------------------------------------
298-
299-
record Lattice c ℓ : Set (suc (c ⊔ ℓ)) where
300-
infixr 7 _∧_
301-
infixr 6 _∨_
302-
infix 4 _≈_
303-
field
304-
Carrier : Set c
305-
_≈_ : Rel Carrier ℓ
306-
_∨_ : Op₂ Carrier
307-
_∧_ : Op₂ Carrier
308-
isLattice : IsLattice _≈_ _∨_ _∧_
309-
310-
open IsLattice isLattice public
311-
312-
setoid : Setoid _ _
313-
setoid = record { isEquivalence = isEquivalence }
314-
315-
316-
record DistributiveLattice c ℓ : Set (suc (c ⊔ ℓ)) where
317-
infixr 7 _∧_
318-
infixr 6 _∨_
319-
infix 4 _≈_
320-
field
321-
Carrier : Set c
322-
_≈_ : Rel Carrier ℓ
323-
_∨_ : Op₂ Carrier
324-
_∧_ : Op₂ Carrier
325-
isDistributiveLattice : IsDistributiveLattice _≈_ _∨_ _∧_
326-
327-
open IsDistributiveLattice isDistributiveLattice public
328-
329-
lattice : Lattice _ _
330-
lattice = record { isLattice = isLattice }
331-
332-
open Lattice lattice public using (setoid)
333-
334-
335277
------------------------------------------------------------------------
336278
-- Bundles with 2 binary operations & 1 element
337279
------------------------------------------------------------------------
@@ -701,30 +643,6 @@ record CommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where
701643
)
702644

703645

704-
record BooleanAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where
705-
infix 8 ¬_
706-
infixr 7 _∧_
707-
infixr 6 _∨_
708-
infix 4 _≈_
709-
field
710-
Carrier : Set c
711-
_≈_ : Rel Carrier ℓ
712-
_∨_ : Op₂ Carrier
713-
_∧_ : Op₂ Carrier
714-
¬_ : Op₁ Carrier
715-
⊤ : Carrier
716-
⊥ : Carrier
717-
isBooleanAlgebra : IsBooleanAlgebra _≈_ _∨_ _∧_ ¬_ ⊤ ⊥
718-
719-
open IsBooleanAlgebra isBooleanAlgebra public
720-
721-
distributiveLattice : DistributiveLattice _ _
722-
distributiveLattice = record { isDistributiveLattice = isDistributiveLattice }
723-
724-
open DistributiveLattice distributiveLattice public
725-
using (setoid; lattice)
726-
727-
728646
------------------------------------------------------------------------
729647
-- DEPRECATED NAMES
730648
------------------------------------------------------------------------

‎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: 184 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,184 @@
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 using
41+
(rawMagma; magma; isMagma; semigroup; isSemigroup; isBand)
42+
43+
record MeetSemilattice c ℓ : Set (suc (c ⊔ ℓ)) where
44+
infixr 7 _∧_
45+
infix 4 _≈_
46+
field
47+
Carrier : Set c
48+
_≈_ : Rel Carrier ℓ
49+
_∧_ : Op₂ Carrier
50+
isMeetSemilattice : IsSemilattice _≈_ _∧_
51+
52+
open IsMeetSemilattice _≈_ isMeetSemilattice public
53+
54+
semilattice : Semilattice c ℓ
55+
semilattice = record { isSemilattice = isMeetSemilattice }
56+
57+
open Semilattice semilattice public using (rawMagma; magma; semigroup; band)
58+
59+
record JoinSemilattice c ℓ : Set (suc (c ⊔ ℓ)) where
60+
infixr 7 _∨_
61+
infix 4 _≈_
62+
field
63+
Carrier : Set c
64+
_≈_ : Rel Carrier ℓ
65+
_∨_ : Op₂ Carrier
66+
isJoinSemilattice : IsSemilattice _≈_ _∨_
67+
68+
open IsJoinSemilattice _≈_ isJoinSemilattice public
69+
70+
semilattice : Semilattice c ℓ
71+
semilattice = record { isSemilattice = isJoinSemilattice }
72+
73+
open Semilattice semilattice public using (rawMagma; magma; semigroup; band)
74+
75+
76+
record BoundedSemilattice c ℓ : Set (suc (c ⊔ ℓ)) where
77+
infixr 7 _∙_
78+
infix 4 _≈_
79+
field
80+
Carrier : Set c
81+
_≈_ : Rel Carrier ℓ
82+
_∙_ : Op₂ Carrier
83+
ε : Carrier
84+
isBoundedSemilattice : IsBoundedSemilattice _≈_ _∙_ ε
85+
86+
open IsBoundedSemilattice _≈_ isBoundedSemilattice public
87+
88+
semilattice : Semilattice c ℓ
89+
semilattice = record { isSemilattice = isSemilattice }
90+
91+
open Semilattice semilattice public using (rawMagma; magma; semigroup; band)
92+
93+
record BoundedMeetSemilattice c ℓ : Set (suc (c ⊔ ℓ)) where
94+
infixr 7 _∧_
95+
infix 4 _≈_
96+
field
97+
Carrier : Set c
98+
_≈_ : Rel Carrier ℓ
99+
_∧_ : Op₂ Carrier
100+
⊤ : Carrier
101+
isBoundedMeetSemilattice : IsBoundedSemilattice _≈_ _∧_ ⊤
102+
103+
open IsBoundedMeetSemilattice _≈_ isBoundedMeetSemilattice public
104+
105+
boundedSemilattice : BoundedSemilattice c ℓ
106+
boundedSemilattice = record
107+
{ isBoundedSemilattice = isBoundedMeetSemilattice }
108+
109+
open BoundedSemilattice boundedSemilattice public
110+
using (rawMagma; magma; semigroup; band; semilattice)
111+
112+
record BoundedJoinSemilattice c ℓ : Set (suc (c ⊔ ℓ)) where
113+
infixr 7 _∨_
114+
infix 4 _≈_
115+
field
116+
Carrier : Set c
117+
_≈_ : Rel Carrier ℓ
118+
_∨_ : Op₂ Carrier
119+
⊥ : Carrier
120+
isBoundedJoinSemilattice : IsBoundedSemilattice _≈_ _∨_ ⊥
121+
122+
open IsBoundedJoinSemilattice _≈_ isBoundedJoinSemilattice public
123+
124+
boundedSemilattice : BoundedSemilattice c ℓ
125+
boundedSemilattice = record
126+
{ isBoundedSemilattice = isBoundedJoinSemilattice }
127+
128+
open BoundedSemilattice boundedSemilattice public
129+
using (rawMagma; magma; semigroup; band; semilattice)
130+
131+
132+
record Lattice c ℓ : Set (suc (c ⊔ ℓ)) where
133+
infixr 7 _∧_
134+
infixr 6 _∨_
135+
infix 4 _≈_
136+
field
137+
Carrier : Set c
138+
_≈_ : Rel Carrier ℓ
139+
_∨_ : Op₂ Carrier
140+
_∧_ : Op₂ Carrier
141+
isLattice : IsLattice _≈_ _∨_ _∧_
142+
143+
open IsLattice isLattice public
144+
145+
146+
record DistributiveLattice c ℓ : Set (suc (c ⊔ ℓ)) where
147+
infixr 7 _∧_
148+
infixr 6 _∨_
149+
infix 4 _≈_
150+
field
151+
Carrier : Set c
152+
_≈_ : Rel Carrier ℓ
153+
_∨_ : Op₂ Carrier
154+
_∧_ : Op₂ Carrier
155+
isDistributiveLattice : IsDistributiveLattice _≈_ _∨_ _∧_
156+
157+
open IsDistributiveLattice isDistributiveLattice public
158+
159+
lattice : Lattice _ _
160+
lattice = record { isLattice = isLattice }
161+
162+
163+
record BooleanAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where
164+
infix 8 ¬_
165+
infixr 7 _∧_
166+
infixr 6 _∨_
167+
infix 4 _≈_
168+
field
169+
Carrier : Set c
170+
_≈_ : Rel Carrier ℓ
171+
_∨_ : Op₂ Carrier
172+
_∧_ : Op₂ Carrier
173+
¬_ : Op₁ Carrier
174+
⊤ : Carrier
175+
⊥ : Carrier
176+
isBooleanAlgebra : IsBooleanAlgebra _≈_ _∨_ _∧_ ¬_ ⊤ ⊥
177+
178+
open IsBooleanAlgebra isBooleanAlgebra public
179+
180+
distributiveLattice : DistributiveLattice _ _
181+
distributiveLattice = record { isDistributiveLattice = isDistributiveLattice }
182+
183+
open DistributiveLattice distributiveLattice public
184+
using (lattice)

0 commit comments

Comments
 (0)