blob: e2ac96495ba724a7a1c05cb104e9e19b08a9ec48 (
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
|
{-# OPTIONS --without-K --safe #-}
module Lattice.Bundle.BoundedDistributive where
open import Algebra using (Op₂)
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; joinSemilattice; meetSemilattice; poset; preorder; setoid)
|
