    ------------------------------------------------------------------------
    -- 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)

    module Relation.Binary.Lattice.Structures
     {a ℓ₁ ℓ₂} {A : Set a}
     (_≈_ : Rel A ℓ₁) -- The underlying equality.
     (_≤_ : Rel A ℓ₂) -- The partial order.
     where

    open import Algebra.Core using (Op₁; Op₂)
    open import Algebra.Definitions using (_DistributesOverˡ_)
    open import Data.Product.Base using (_×_; _,_)
    open import Level using (suc; _⊔_)
    open import Relation.Binary.Definitions using (Minimum; Maximum)
    open import Relation.Binary.Lattice.Definitions
      using (Supremum; Infimum; Exponential)
    open import Relation.Binary.Structures using (IsPartialOrder)

    ------------------------------------------------------------------------
    -- 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