module Relation.Binary.Lattice where
open import Algebra.FunctionProperties
open import Data.Product
open import Function using (flip)
open import Level
open import Relation.Binary
import Relation.Binary.PropositionalEquality as PropEq
Supremum : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Op₂ A → Set _
Supremum _≤_ _∨_ =
∀ x y → x ≤ (x ∨ y) × y ≤ (x ∨ y) × ∀ z → x ≤ z → y ≤ z → (x ∨ y) ≤ z
Infimum : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Op₂ A → Set _
Infimum _≤_ = Supremum (flip _≤_)
Maximum : ∀ {a ℓ} {A : Set a} → Rel A ℓ → A → Set _
Maximum _≤_ ⊤ = ∀ x → x ≤ ⊤
Minimum : ∀ {a ℓ} {A : Set a} → Rel A ℓ → A → Set _
Minimum _≤_ = Maximum (flip _≤_)
record IsJoinSemilattice {a ℓ₁ ℓ₂} {A : Set a}
(_≈_ : Rel A ℓ₁)
(_≤_ : Rel A ℓ₂)
(_∨_ : Op₂ A)
: Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isPartialOrder : IsPartialOrder _≈_ _≤_
supremum : Supremum _≤_ _∨_
open IsPartialOrder isPartialOrder public
record JoinSemilattice c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 4 _≈_ _≤_
infixr 6 _∨_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ₁
_≤_ : Rel Carrier ℓ₂
_∨_ : Op₂ Carrier
isJoinSemilattice : IsJoinSemilattice _≈_ _≤_ _∨_
open IsJoinSemilattice isJoinSemilattice public
poset : Poset c ℓ₁ ℓ₂
poset = record { isPartialOrder = isPartialOrder }
open Poset poset public using (preorder)
record IsMeetSemilattice {a ℓ₁ ℓ₂} {A : Set a}
(_≈_ : Rel A ℓ₁)
(_≤_ : Rel A ℓ₂)
(_∧_ : Op₂ A)
: Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isPartialOrder : IsPartialOrder _≈_ _≤_
infimum : Infimum _≤_ _∧_
open IsPartialOrder isPartialOrder public
record MeetSemilattice c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 4 _≈_ _≤_
infixr 7 _∧_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ₁
_≤_ : Rel Carrier ℓ₂
_∧_ : Op₂ Carrier
isMeetSemilattice : IsMeetSemilattice _≈_ _≤_ _∧_
open IsMeetSemilattice isMeetSemilattice public
poset : Poset c ℓ₁ ℓ₂
poset = record { isPartialOrder = isPartialOrder }
open Poset poset public using (preorder)
record IsBoundedJoinSemilattice {a ℓ₁ ℓ₂} {A : Set a}
(_≈_ : Rel A ℓ₁)
(_≤_ : Rel A ℓ₂)
(_∨_ : Op₂ A)
(⊥ : A)
: Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isJoinSemilattice : IsJoinSemilattice _≈_ _≤_ _∨_
minimum : Minimum _≤_ ⊥
open IsJoinSemilattice isJoinSemilattice public
record BoundedJoinSemilattice c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 4 _≈_ _≤_
infixr 6 _∨_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ₁
_≤_ : Rel Carrier ℓ₂
_∨_ : Op₂ Carrier
⊥ : Carrier
isBoundedJoinSemilattice : IsBoundedJoinSemilattice _≈_ _≤_ _∨_ ⊥
open IsBoundedJoinSemilattice isBoundedJoinSemilattice public
joinSemiLattice : JoinSemilattice c ℓ₁ ℓ₂
joinSemiLattice = record { isJoinSemilattice = isJoinSemilattice }
open JoinSemilattice joinSemiLattice public using (preorder; poset)
record IsBoundedMeetSemilattice {a ℓ₁ ℓ₂} {A : Set a}
(_≈_ : Rel A ℓ₁)
(_≤_ : Rel A ℓ₂)
(_∧_ : Op₂ A)
(⊤ : A)
: Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isMeetSemilattice : IsMeetSemilattice _≈_ _≤_ _∧_
maximum : Maximum _≤_ ⊤
open IsMeetSemilattice isMeetSemilattice public
record BoundedMeetSemilattice c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 4 _≈_ _≤_
infixr 7 _∧_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ₁
_≤_ : Rel Carrier ℓ₂
_∧_ : Op₂ Carrier
⊤ : Carrier
isBoundedMeetSemilattice : IsBoundedMeetSemilattice _≈_ _≤_ _∧_ ⊤
open IsBoundedMeetSemilattice isBoundedMeetSemilattice public
meetSemiLattice : MeetSemilattice c ℓ₁ ℓ₂
meetSemiLattice = record { isMeetSemilattice = isMeetSemilattice }
open MeetSemilattice meetSemiLattice public using (preorder; poset)
record IsLattice {a ℓ₁ ℓ₂} {A : Set a}
(_≈_ : Rel A ℓ₁)
(_≤_ : Rel A ℓ₂)
(_∨_ : Op₂ A)
(_∧_ : Op₂ A)
: Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isPartialOrder : IsPartialOrder _≈_ _≤_
supremum : Supremum _≤_ _∨_
infimum : Infimum _≤_ _∧_
isJoinSemilattice : IsJoinSemilattice _≈_ _≤_ _∨_
isJoinSemilattice = record
{ isPartialOrder = isPartialOrder
; supremum = supremum
}
isMeetSemilattice : IsMeetSemilattice _≈_ _≤_ _∧_
isMeetSemilattice = record
{ isPartialOrder = isPartialOrder
; infimum = infimum
}
open IsPartialOrder isPartialOrder public
record Lattice c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 4 _≈_ _≤_
infixr 6 _∨_
infixr 7 _∧_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ₁
_≤_ : Rel Carrier ℓ₂
_∨_ : Op₂ Carrier
_∧_ : Op₂ Carrier
isLattice : IsLattice _≈_ _≤_ _∨_ _∧_
open IsLattice isLattice public
joinSemilattice : JoinSemilattice c ℓ₁ ℓ₂
joinSemilattice = record { isJoinSemilattice = isJoinSemilattice }
meetSemilattice : MeetSemilattice c ℓ₁ ℓ₂
meetSemilattice = record { isMeetSemilattice = isMeetSemilattice }
open JoinSemilattice joinSemilattice public using (poset; preorder)
record IsBoundedLattice {a ℓ₁ ℓ₂} {A : Set a}
(_≈_ : Rel A ℓ₁)
(_≤_ : Rel A ℓ₂)
(_∨_ : Op₂ A)
(_∧_ : Op₂ A)
(⊤ : A)
(⊥ : A)
: Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isLattice : IsLattice _≈_ _≤_ _∨_ _∧_
maximum : Maximum _≤_ ⊤
minimum : Minimum _≤_ ⊥
open IsLattice isLattice public
isBoundedJoinSemilattice : IsBoundedJoinSemilattice _≈_ _≤_ _∨_ ⊥
isBoundedJoinSemilattice = record
{ isJoinSemilattice = isJoinSemilattice
; minimum = minimum
}
isBoundedMeetSemilattice : IsBoundedMeetSemilattice _≈_ _≤_ _∧_ ⊤
isBoundedMeetSemilattice = record
{ isMeetSemilattice = isMeetSemilattice
; maximum = maximum
}
record BoundedLattice c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 4 _≈_ _≤_
infixr 6 _∨_
infixr 7 _∧_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ₁
_≤_ : Rel Carrier ℓ₂
_∨_ : Op₂ Carrier
_∧_ : Op₂ Carrier
⊤ : Carrier
⊥ : Carrier
isBoundedLattice : IsBoundedLattice _≈_ _≤_ _∨_ _∧_ ⊤ ⊥
open IsBoundedLattice isBoundedLattice public
boundedJoinSemilattice : BoundedJoinSemilattice c ℓ₁ ℓ₂
boundedJoinSemilattice = record
{ isBoundedJoinSemilattice = isBoundedJoinSemilattice }
boundedMeetSemilattice : BoundedMeetSemilattice c ℓ₁ ℓ₂
boundedMeetSemilattice = record
{ isBoundedMeetSemilattice = isBoundedMeetSemilattice }