blob: c40de30694495b49d75449fbf666c18c6f2fabce (
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
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
|
------------------------------------------------------------------------
-- Agda Helium
--
-- Definitions of decidable algebraic structures like monoids and rings
-- (packed in records together with sets, operations, etc.)
------------------------------------------------------------------------
{-# OPTIONS --without-K --safe #-}
module Helium.Algebra.Decidable.Bundles where
open import Algebra.Lattice.Bundles using (RawLattice)
open import Algebra.Core
open import Helium.Algebra.Decidable.Structures
open import Level using (suc; _⊔_)
open import Relation.Binary.Bundles using (DecSetoid)
open import Relation.Binary.Core using (Rel)
record Lattice c ℓ : Set (suc (c ⊔ ℓ)) where
infixr 7 _∧_
infixr 6 _∨_
infix 4 _≈_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ
_∨_ : Op₂ Carrier
_∧_ : Op₂ Carrier
isLattice : IsLattice _≈_ _∨_ _∧_
open IsLattice isLattice public
rawLattice : RawLattice c ℓ
rawLattice = record
{ _≈_ = _≈_
; _∧_ = _∧_
; _∨_ = _∨_
}
open RawLattice rawLattice public
using (∨-rawMagma; ∧-rawMagma)
decSetoid : DecSetoid _ _
decSetoid = record { isDecEquivalence = isDecEquivalence }
open DecSetoid decSetoid public
using (_≉_; setoid)
record DistributiveLattice c ℓ : Set (suc (c ⊔ ℓ)) where
infixr 7 _∧_
infixr 6 _∨_
infix 4 _≈_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ
_∨_ : Op₂ Carrier
_∧_ : Op₂ Carrier
isDistributiveLattice : IsDistributiveLattice _≈_ _∨_ _∧_
open IsDistributiveLattice isDistributiveLattice public
lattice : Lattice _ _
lattice = record { isLattice = isLattice }
open Lattice lattice public
using (_≉_; setoid; decSetoid; ∨-rawMagma; ∧-rawMagma; rawLattice)
record RawBooleanAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where
infix 8 ¬_
infixr 7 _∧_
infixr 6 _∨_
infix 4 _≈_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ
_∧_ : Op₂ Carrier
_∨_ : Op₂ Carrier
¬_ : Op₁ Carrier
⊤ : Carrier
⊥ : Carrier
rawLattice : RawLattice c ℓ
rawLattice = record { _≈_ = _≈_; _∨_ = _∨_; _∧_ = _∧_ }
open RawLattice rawLattice public
using (_≉_; ∨-rawMagma; ∧-rawMagma)
record BooleanAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where
infix 8 ¬_
infixr 7 _∧_
infixr 6 _∨_
infix 4 _≈_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ
_∨_ : Op₂ Carrier
_∧_ : Op₂ Carrier
¬_ : Op₁ Carrier
⊤ : Carrier
⊥ : Carrier
isBooleanAlgebra : IsBooleanAlgebra _≈_ _∨_ _∧_ ¬_ ⊤ ⊥
open IsBooleanAlgebra isBooleanAlgebra public
distributiveLattice : DistributiveLattice _ _
distributiveLattice = record { isDistributiveLattice = isDistributiveLattice }
open DistributiveLattice distributiveLattice public
using (_≉_; setoid; decSetoid; ∨-rawMagma; ∧-rawMagma; rawLattice; lattice)
|
