blob: 4380cc5ac124ddf0b499de11ab13083de3b3371b (
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
|
------------------------------------------------------------------------
-- Agda Helium
--
-- Some decidable algebraic structures (not packed up with sets,
-- operations, etc.)
------------------------------------------------------------------------
{-# OPTIONS --without-K --safe #-}
open import Relation.Binary.Core using (Rel)
module Helium.Algebra.Decidable.Structures
{a ℓ} {A : Set a} -- The underlying set
(_≈_ : Rel A ℓ) -- The underlying equality relation
where
open import Algebra.Core
open import Algebra.Definitions (_≈_)
open import Data.Product using (proj₁; proj₂)
open import Level using (_⊔_)
open import Relation.Binary.Structures using (IsDecEquivalence)
record IsLattice (∨ ∧ : Op₂ A) : Set (a ⊔ ℓ) where
field
isDecEquivalence : IsDecEquivalence _≈_
∨-comm : Commutative ∨
∨-assoc : Associative ∨
∨-cong : Congruent₂ ∨
∧-comm : Commutative ∧
∧-assoc : Associative ∧
∧-cong : Congruent₂ ∧
absorptive : Absorptive ∨ ∧
open IsDecEquivalence isDecEquivalence public
∨-absorbs-∧ : ∨ Absorbs ∧
∨-absorbs-∧ = proj₁ absorptive
∧-absorbs-∨ : ∧ Absorbs ∨
∧-absorbs-∨ = proj₂ absorptive
∧-congˡ : LeftCongruent ∧
∧-congˡ y≈z = ∧-cong refl y≈z
∧-congʳ : RightCongruent ∧
∧-congʳ y≈z = ∧-cong y≈z refl
∨-congˡ : LeftCongruent ∨
∨-congˡ y≈z = ∨-cong refl y≈z
∨-congʳ : RightCongruent ∨
∨-congʳ y≈z = ∨-cong y≈z refl
record IsDistributiveLattice (∨ ∧ : Op₂ A) : Set (a ⊔ ℓ) where
field
isLattice : IsLattice ∨ ∧
∨-distrib-∧ : ∨ DistributesOver ∧
open IsLattice isLattice public
∨-distribˡ-∧ : ∨ DistributesOverˡ ∧
∨-distribˡ-∧ = proj₁ ∨-distrib-∧
∨-distribʳ-∧ : ∨ DistributesOverʳ ∧
∨-distribʳ-∧ = proj₂ ∨-distrib-∧
record IsBooleanAlgebra
(∨ ∧ : Op₂ A) (¬ : Op₁ A) (⊤ ⊥ : A) : Set (a ⊔ ℓ) where
field
isDistributiveLattice : IsDistributiveLattice ∨ ∧
∨-complement : Inverse ⊤ ¬ ∨
∧-complement : Inverse ⊥ ¬ ∧
¬-cong : Congruent₁ ¬
open IsDistributiveLattice isDistributiveLattice public
∨-complementˡ : LeftInverse ⊤ ¬ ∨
∨-complementˡ = proj₁ ∨-complement
∨-complementʳ : RightInverse ⊤ ¬ ∨
∨-complementʳ = proj₂ ∨-complement
∧-complementˡ : LeftInverse ⊥ ¬ ∧
∧-complementˡ = proj₁ ∧-complement
∧-complementʳ : RightInverse ⊥ ¬ ∧
∧-complementʳ = proj₂ ∧-complement
|
