    ------------------------------------------------------------------------
    -- 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 using (Op₁; Op₂)
    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