{-# 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}
(_≈_ : Rel A ℓ)
where
open import Algebra.Definitions _≈_
open import Algebra.Lattice.Structures _≈_
private
variable
∧ ∨ : Op₂ A
¬ : Op₁ A
⊤ ⊥ : A
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₂)
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ʳʲᵐ)
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ʳ)