{-# OPTIONS --without-K --safe #-}
open import Relation.Binary
module Relation.Binary.Lattice.Structures
{a ℓ₁ ℓ₂} {A : Set a}
(_≈_ : Rel A ℓ₁)
(_≤_ : Rel A ℓ₂)
where
open import Algebra.Core
open import Algebra.Definitions
open import Data.Product using (_×_; _,_)
open import Level using (suc; _⊔_)
open import Relation.Binary.Lattice.Definitions
record IsJoinSemilattice (_∨_ : Op₂ A)
: Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isPartialOrder : IsPartialOrder _≈_ _≤_
supremum : Supremum _≤_ _∨_
x≤x∨y : ∀ x y → x ≤ (x ∨ y)
x≤x∨y x y = let pf , _ , _ = supremum x y in pf
y≤x∨y : ∀ x y → y ≤ (x ∨ y)
y≤x∨y x y = let _ , pf , _ = supremum x y in pf
∨-least : ∀ {x y z} → x ≤ z → y ≤ z → (x ∨ y) ≤ z
∨-least {x} {y} {z} = let _ , _ , pf = supremum x y in pf z
open IsPartialOrder isPartialOrder public
record IsBoundedJoinSemilattice (_∨_ : Op₂ A)
(⊥ : A)
: Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isJoinSemilattice : IsJoinSemilattice _∨_
minimum : Minimum _≤_ ⊥
open IsJoinSemilattice isJoinSemilattice public
record IsMeetSemilattice (_∧_ : Op₂ A)
: Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isPartialOrder : IsPartialOrder _≈_ _≤_
infimum : Infimum _≤_ _∧_
x∧y≤x : ∀ x y → (x ∧ y) ≤ x
x∧y≤x x y = let pf , _ , _ = infimum x y in pf
x∧y≤y : ∀ x y → (x ∧ y) ≤ y
x∧y≤y x y = let _ , pf , _ = infimum x y in pf
∧-greatest : ∀ {x y z} → x ≤ y → x ≤ z → x ≤ (y ∧ z)
∧-greatest {x} {y} {z} = let _ , _ , pf = infimum y z in pf x
open IsPartialOrder isPartialOrder public
record IsBoundedMeetSemilattice (_∧_ : Op₂ A)
(⊤ : A)
: Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isMeetSemilattice : IsMeetSemilattice _∧_
maximum : Maximum _≤_ ⊤
open IsMeetSemilattice isMeetSemilattice public
record IsLattice (_∨_ : 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 IsJoinSemilattice isJoinSemilattice public
using (x≤x∨y; y≤x∨y; ∨-least)
open IsMeetSemilattice isMeetSemilattice public
using (x∧y≤x; x∧y≤y; ∧-greatest)
open IsPartialOrder isPartialOrder public
record IsDistributiveLattice (_∨_ : Op₂ A)
(_∧_ : Op₂ A)
: Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isLattice : IsLattice _∨_ _∧_
∧-distribˡ-∨ : _DistributesOverˡ_ _≈_ _∧_ _∨_
open IsLattice isLattice public
record IsBoundedLattice (_∨_ : 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 IsHeytingAlgebra (_∨_ : Op₂ A)
(_∧_ : Op₂ A)
(_⇨_ : Op₂ A)
(⊤ : A)
(⊥ : A)
: Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isBoundedLattice : IsBoundedLattice _∨_ _∧_ ⊤ ⊥
exponential : Exponential _≤_ _∧_ _⇨_
transpose-⇨ : ∀ {w x y} → (w ∧ x) ≤ y → w ≤ (x ⇨ y)
transpose-⇨ {w} {x} {y} = let pf , _ = exponential w x y in pf
transpose-∧ : ∀ {w x y} → w ≤ (x ⇨ y) → (w ∧ x) ≤ y
transpose-∧ {w} {x} {y} = let _ , pf = exponential w x y in pf
open IsBoundedLattice isBoundedLattice public
record IsBooleanAlgebra (_∨_ : Op₂ A)
(_∧_ : Op₂ A)
(¬_ : Op₁ A)
(⊤ : A)
(⊥ : A)
: Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
infixr 5 _⇨_
_⇨_ : Op₂ A
x ⇨ y = (¬ x) ∨ y
field
isHeytingAlgebra : IsHeytingAlgebra _∨_ _∧_ _⇨_ ⊤ ⊥
open IsHeytingAlgebra isHeytingAlgebra public