    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Definitions for order-theoretic lattices
    ------------------------------------------------------------------------

    -- The contents of this module should be accessed via
    -- `Relation.Binary.Lattice`.

    {-# OPTIONS --cubical-compatible --safe #-}

    module Relation.Binary.Lattice.Definitions where

    open import Algebra.Core using (Op₁; Op₂)
    open import Data.Product.Base using (_×_; _,_)
    open import Function.Base using (flip)
    open import Level using (Level)
    open import Relation.Binary.Core using (Rel)

    private
      variable
        a ℓ : Level
        A : Set a

    ------------------------------------------------------------------------
    -- Relationships between orders and operators

    Supremum : Rel A ℓ → Op₂ A → Set _
    Supremum _≤_ _∨_ =
      ∀ x y → x ≤ (x ∨ y) × y ≤ (x ∨ y) × ∀ z → x ≤ z → y ≤ z → (x ∨ y) ≤ z

    Infimum : Rel A ℓ → Op₂ A → Set _
    Infimum _≤_ = Supremum (flip _≤_)

    Exponential : Rel A ℓ → Op₂ A → Op₂ A → Set _
    Exponential _≤_ _∧_ _⇨_ =
      ∀ w x y → ((w ∧ x) ≤ y → w ≤ (x ⇨ y)) × (w ≤ (x ⇨ y) → (w ∧ x) ≤ y)