------------------------------------------------------------------------
-- The Agda standard library
--
-- Some lattice-like structures defined by properties of _∧_ and _∨_
-- (not packed up with sets, operations, etc.)
--
-- For lattices defined via an order relation, see
-- Relation.Binary.Lattice.
------------------------------------------------------------------------
 
-- The contents of this module should be accessed via `Algebra.Lattice`,
-- unless you want to parameterise it via the equality relation.
 
{-# OPTIONS --cubical-compatible --safe #-}
 
open import Algebra.Core
open import Data.Product.Base using (proj₁; proj₂)
open import Level using (_⊔_)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.Structures using (IsEquivalence)
 
module Algebra.Lattice.Structures
  {a ℓ} {A : Set a}  -- The underlying set
  (_≈_ : Rel A ℓ)    -- The underlying equality relation
  where
 
open import Algebra.Definitions _≈_
open import Algebra.Structures _≈_
 
------------------------------------------------------------------------
-- Structures with 1 binary operation
 
IsSemilattice = IsCommutativeBand
module IsSemilattice {∙} (L : IsSemilattice ∙) where
  open IsCommutativeBand L public
    using (isBand; comm)
  open IsBand isBand public
 
-- Used to bring names appropriate for a meet semilattice into scope.
IsMeetSemilattice = IsSemilattice
module IsMeetSemilattice {∧} (L : IsMeetSemilattice ∧) where
  open IsSemilattice L public
    renaming
    ( ∙-cong  to ∧-cong
    ; ∙-congˡ to ∧-congˡ
    ; ∙-congʳ to ∧-congʳ
    )
 
-- Used to bring names appropriate for a join semilattice into scope.
IsJoinSemilattice = IsSemilattice
module IsJoinSemilattice {∨} (L : IsJoinSemilattice ∨) where
  open IsSemilattice L public
    renaming
    ( ∙-cong  to ∨-cong
    ; ∙-congˡ to ∨-congˡ
    ; ∙-congʳ to ∨-congʳ
    )
 
------------------------------------------------------------------------
-- Structures with 1 binary operation & 1 element
 
-- A bounded semi-lattice is the same thing as an idempotent commutative
-- monoid.
IsBoundedSemilattice = IsIdempotentCommutativeMonoid
module IsBoundedSemilattice {∙ ε} (L : IsBoundedSemilattice ∙ ε) where
 
  open IsIdempotentCommutativeMonoid L public
    renaming (isCommutativeBand to isSemilattice)
 
 
-- Used to bring names appropriate for a bounded meet semilattice
-- into scope.
IsBoundedMeetSemilattice = IsBoundedSemilattice
module IsBoundedMeetSemilattice {∧ ⊤} (L : IsBoundedMeetSemilattice ∧ ⊤)
  where
 
  open IsBoundedSemilattice L public
    using (identity; identityˡ; identityʳ)
    renaming (isSemilattice to isMeetSemilattice)
 
  open IsMeetSemilattice isMeetSemilattice public
 
 
-- Used to bring names appropriate for a bounded join semilattice
-- into scope.
IsBoundedJoinSemilattice = IsBoundedSemilattice
module IsBoundedJoinSemilattice {∨ ⊥} (L : IsBoundedJoinSemilattice ∨ ⊥)
  where
 
  open IsBoundedSemilattice L public
    using (identity; identityˡ; identityʳ)
    renaming (isSemilattice to isJoinSemilattice)
 
  open IsJoinSemilattice isJoinSemilattice public
 
------------------------------------------------------------------------
-- Structures with 2 binary operations
 
-- Note that `IsLattice` is not defined in terms of `IsMeetSemilattice`
-- and `IsJoinSemilattice` for two reasons:
--   1) it would result in a structure with two *different* proofs that
--   the equality relation `≈` is an equivalence relation.
--   2) the idempotence laws of ∨ and ∧ can be derived from the
--   absorption laws, which makes the corresponding "idem" fields
--   redundant.
--
-- It is possible to construct the `IsLattice` record from
-- `IsMeetSemilattice` and `IsJoinSemilattice` via the `IsLattice₂`
-- record found in `Algebra.Lattice.Structures.Biased`.
--
-- The derived idempotence laws are stated and proved in
-- `Algebra.Lattice.Properties.Lattice` along with the fact that every
-- lattice consists of two semilattices.
 
record IsLattice (∨ ∧ : Op₂ A) : Set (a ⊔ ℓ) where
  field
    isEquivalence : IsEquivalence _≈_
    ∨-comm        : Commutative ∨
    ∨-assoc       : Associative ∨
    ∨-cong        : Congruent₂ ∨
    ∧-comm        : Commutative ∧
    ∧-assoc       : Associative ∧
    ∧-cong        : Congruent₂ ∧
    absorptive    : Absorptive ∨ ∧
 
  open IsEquivalence isEquivalence public
 
  ∨-absorbs-∧ : ∨ Absorbs ∧
  ∨-absorbs-∧ = proj₁ absorptive
 
  ∧-absorbs-∨ : ∧ Absorbs ∨
  ∧-absorbs-∨ = proj₂ absorptive
 
  ∧-congˡ : LeftCongruent ∧
  ∧-congˡ y≈z = ∧-cong refl y≈z
 
  ∧-congʳ : RightCongruent ∧
  ∧-congʳ y≈z = ∧-cong y≈z refl
 
  ∨-congˡ : LeftCongruent ∨
  ∨-congˡ y≈z = ∨-cong refl y≈z
 
  ∨-congʳ : RightCongruent ∨
  ∨-congʳ y≈z = ∨-cong y≈z refl
 
 
record IsDistributiveLattice (∨ ∧ : Op₂ A) : Set (a ⊔ ℓ) where
  field
    isLattice   : IsLattice ∨ ∧
    ∨-distrib-∧ : ∨ DistributesOver ∧
    ∧-distrib-∨ : ∧ DistributesOver ∨
 
  open IsLattice isLattice public
 
  ∨-distribˡ-∧ : ∨ DistributesOverˡ ∧
  ∨-distribˡ-∧ = proj₁ ∨-distrib-∧
 
  ∨-distribʳ-∧ : ∨ DistributesOverʳ ∧
  ∨-distribʳ-∧ = proj₂ ∨-distrib-∧
 
  ∧-distribˡ-∨ : ∧ DistributesOverˡ ∨
  ∧-distribˡ-∨ = proj₁ ∧-distrib-∨
 
  ∧-distribʳ-∨ : ∧ DistributesOverʳ ∨
  ∧-distribʳ-∨ = proj₂ ∧-distrib-∨
 
------------------------------------------------------------------------
-- Structures with 2 binary ops, 1 unary op and 2 elements.
 
record IsBooleanAlgebra (∨ ∧ : Op₂ A) (¬ : Op₁ A) (⊤ ⊥ : A) : Set (a ⊔ ℓ)
  where
 
  field
    isDistributiveLattice : IsDistributiveLattice ∨ ∧
    ∨-complement          : Inverse ⊤ ¬ ∨
    ∧-complement          : Inverse ⊥ ¬ ∧
    ¬-cong                : Congruent₁ ¬
 
  open IsDistributiveLattice isDistributiveLattice public
 
  ∨-complementˡ : LeftInverse ⊤ ¬ ∨
  ∨-complementˡ = proj₁ ∨-complement
 
  ∨-complementʳ : RightInverse ⊤ ¬ ∨
  ∨-complementʳ = proj₂ ∨-complement
 
  ∧-complementˡ : LeftInverse ⊥ ¬ ∧
  ∧-complementˡ = proj₁ ∧-complement
 
  ∧-complementʳ : RightInverse ⊥ ¬ ∧
  ∧-complementʳ = proj₂ ∧-complement