------------------------------------------------------------------------ -- The Agda standard library -- -- Some biased records for lattice-like structures. Such records are -- often easier to construct, but are suboptimal to use more widely and -- should be converted to the standard record definitions immediately -- using the provided conversion functions. ------------------------------------------------------------------------ -- The contents of this module should be accessed via `Algebra.Lattice`, -- unless you want to parameterise it via the equality relation. {-# OPTIONS --without-K --safe #-} open import Algebra.Core open import Algebra.Consequences.Setoid open import Data.Product using (proj₁; proj₂) open import Level using (_⊔_) open import Relation.Binary using (Rel; Setoid; IsEquivalence) module Algebra.Lattice.Structures.Biased {a ℓ} {A : Set a} -- The underlying set (_≈_ : Rel A ℓ) -- The underlying equality relation where open import Algebra.Definitions _≈_ open import Algebra.Lattice.Structures _≈_ private variable ∧ ∨ : Op₂ A ¬ : Op₁ A ⊤ ⊥ : A ------------------------------------------------------------------------ -- Lattice -- An alternative form of `IsLattice` defined in terms of -- `IsJoinSemilattice` and `IsMeetLattice`. This form may be desirable -- to use when constructing a lattice object as it requires fewer -- arguments, but is often a mistake to use as an argument as it -- contains two, *potentially different*, proofs that the equality -- relation _≈_ is an equivalence. record IsLattice₂ (∨ ∧ : Op₂ A) : Set (a ⊔ ℓ) where field isJoinSemilattice : IsJoinSemilattice ∨ isMeetSemilattice : IsMeetSemilattice ∧ absorptive : Absorptive ∨ ∧ module ML = IsMeetSemilattice isMeetSemilattice module JL = IsJoinSemilattice isJoinSemilattice isLattice₂ : IsLattice ∨ ∧ isLattice₂ = record { isEquivalence = ML.isEquivalence ; ∨-comm = JL.comm ; ∨-assoc = JL.assoc ; ∨-cong = JL.∨-cong ; ∧-comm = ML.comm ; ∧-assoc = ML.assoc ; ∧-cong = ML.∧-cong ; absorptive = absorptive } open IsLattice₂ public using (isLattice₂) ------------------------------------------------------------------------ -- DistributiveLattice -- A version of distributive lattice that is biased towards the (r)ight -- distributivity law for (j)oin and (m)eet. record IsDistributiveLatticeʳʲᵐ (∨ ∧ : Op₂ A) : Set (a ⊔ ℓ) where field isLattice : IsLattice ∨ ∧ ∨-distribʳ-∧ : ∨ DistributesOverʳ ∧ open IsLattice isLattice public setoid : Setoid a ℓ setoid = record { isEquivalence = isEquivalence } ∨-distrib-∧ = comm+distrʳ⇒distr setoid ∧-cong ∨-comm ∨-distribʳ-∧ ∧-distribˡ-∨ = distrib+absorbs⇒distribˡ setoid ∧-cong ∧-assoc ∨-comm ∧-absorbs-∨ ∨-absorbs-∧ ∨-distrib-∧ ∧-distrib-∨ = comm+distrˡ⇒distr setoid ∨-cong ∧-comm ∧-distribˡ-∨ isDistributiveLatticeʳʲᵐ : IsDistributiveLattice ∨ ∧ isDistributiveLatticeʳʲᵐ = record { isLattice = isLattice ; ∨-distrib-∧ = ∨-distrib-∧ ; ∧-distrib-∨ = ∧-distrib-∨ } open IsDistributiveLatticeʳʲᵐ public using (isDistributiveLatticeʳʲᵐ) ------------------------------------------------------------------------ -- BooleanAlgebra -- A (r)ight biased version of a boolean algebra. record IsBooleanAlgebraʳ (∨ ∧ : Op₂ A) (¬ : Op₁ A) (⊤ ⊥ : A) : Set (a ⊔ ℓ) where field isDistributiveLattice : IsDistributiveLattice ∨ ∧ ∨-complementʳ : RightInverse ⊤ ¬ ∨ ∧-complementʳ : RightInverse ⊥ ¬ ∧ ¬-cong : Congruent₁ ¬ open IsDistributiveLattice isDistributiveLattice public setoid : Setoid a ℓ setoid = record { isEquivalence = isEquivalence } isBooleanAlgebraʳ : IsBooleanAlgebra ∨ ∧ ¬ ⊤ ⊥ isBooleanAlgebraʳ = record { isDistributiveLattice = isDistributiveLattice ; ∨-complement = comm+invʳ⇒inv setoid ∨-comm ∨-complementʳ ; ∧-complement = comm+invʳ⇒inv setoid ∧-comm ∧-complementʳ ; ¬-cong = ¬-cong } open IsBooleanAlgebraʳ public using (isBooleanAlgebraʳ)