------------------------------------------------------------------------ -- The Agda standard library -- -- Structures for order-theoretic lattices ------------------------------------------------------------------------ -- The contents of this module should be accessed via -- `Relation.Binary.Lattice`. {-# OPTIONS --cubical-compatible --safe #-} open import Relation.Binary.Core using (Rel) open import Relation.Binary.Structures using (IsPartialOrder) open import Relation.Binary.Definitions using (Minimum; Maximum) module Relation.Binary.Lattice.Structures {a ℓ₁ ℓ₂} {A : Set a} (_≈_ : Rel A ℓ₁) -- The underlying equality. (_≤_ : Rel A ℓ₂) -- The partial order. where open import Algebra.Core open import Algebra.Definitions open import Data.Product.Base using (_×_; _,_) open import Level using (suc; _⊔_) open import Relation.Binary.Lattice.Definitions ------------------------------------------------------------------------ -- Join semilattices record IsJoinSemilattice (_∨_ : Op₂ A) -- The join operation. : 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) -- The join operation. (⊥ : A) -- The minimum. : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field isJoinSemilattice : IsJoinSemilattice _∨_ minimum : Minimum _≤_ ⊥ open IsJoinSemilattice isJoinSemilattice public ------------------------------------------------------------------------ -- Meet semilattices record IsMeetSemilattice (_∧_ : Op₂ A) -- The meet operation. : 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) -- The join operation. (⊤ : A) -- The maximum. : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field isMeetSemilattice : IsMeetSemilattice _∧_ maximum : Maximum _≤_ ⊤ open IsMeetSemilattice isMeetSemilattice public ------------------------------------------------------------------------ -- Lattices record IsLattice (_∨_ : Op₂ A) -- The join operation. (_∧_ : Op₂ A) -- The meet operation. : 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) -- The join operation. (_∧_ : Op₂ A) -- The meet operation. : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field isLattice : IsLattice _∨_ _∧_ ∧-distribˡ-∨ : _DistributesOverˡ_ _≈_ _∧_ _∨_ open IsLattice isLattice public record IsBoundedLattice (_∨_ : Op₂ A) -- The join operation. (_∧_ : Op₂ A) -- The meet operation. (⊤ : A) -- The maximum. (⊥ : A) -- The minimum. : 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 } ------------------------------------------------------------------------ -- Heyting algebras (a bounded lattice with exponential operator) record IsHeytingAlgebra (_∨_ : Op₂ A) -- The join operation. (_∧_ : Op₂ A) -- The meet operation. (_⇨_ : Op₂ A) -- The exponential operation. (⊤ : A) -- The maximum. (⊥ : A) -- The minimum. : 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 ------------------------------------------------------------------------ -- Boolean algebras (a specialized Heyting algebra) record IsBooleanAlgebra (_∨_ : Op₂ A) -- The join operation. (_∧_ : Op₂ A) -- The meet operation. (¬_ : Op₁ A) -- The negation operation. (⊤ : A) -- The maximum. (⊥ : A) -- The minimum. : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where infixr 5 _⇨_ _⇨_ : Op₂ A x ⇨ y = (¬ x) ∨ y field isHeytingAlgebra : IsHeytingAlgebra _∨_ _∧_ _⇨_ ⊤ ⊥ open IsHeytingAlgebra isHeytingAlgebra public