    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Conversion of binary operators to binary relations via the left
    -- natural order.
    ------------------------------------------------------------------------

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

    open import Algebra.Core using (Op₂)
    open import Relation.Binary.Core using (Rel; _⇒_)

    module Relation.Binary.Construct.NaturalOrder.Left
      {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) (_∙_ : Op₂ A) where

    open import Data.Product.Base using (_,_; _×_)
    open import Data.Sum.Base using (inj₁; inj₂; map)
    open import Relation.Binary.Bundles
      using (Preorder; Poset; DecPoset; TotalOrder; DecTotalOrder)
    open import Relation.Binary.Structures
      using (IsEquivalence; IsPreorder; IsPartialOrder; IsDecPartialOrder
            ; IsTotalOrder; IsDecTotalOrder)
    open import Relation.Binary.Definitions
      using (Symmetric; Transitive; Reflexive; Antisymmetric; Total; _Respectsʳ_
            ; _Respectsˡ_; _Respects₂_; Decidable)
    open import Relation.Nullary.Negation using (¬_)
    import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
    open import Relation.Binary.Lattice using (Infimum)

    open import Algebra.Definitions _≈_
    open import Algebra.Structures _≈_
    open import Algebra.Lattice.Structures _≈_

    ------------------------------------------------------------------------
    -- Definition

    infix 4 _≤_

    _≤_ : Rel A ℓ
    x ≤ y = x ≈ (x ∙ y)

    ------------------------------------------------------------------------
    -- Relational properties

    reflexive : IsMagma _∙_ → Idempotent _∙_ → _≈_ ⇒ _≤_
    reflexive magma idem {x} {y} x≈y = begin
      x     ≈⟨ sym (idem x) ⟩
      x ∙ x ≈⟨ ∙-cong refl x≈y ⟩
      x ∙ y ∎
      where open IsMagma magma; open ≈-Reasoning setoid

    refl : Symmetric _≈_ → Idempotent _∙_ → Reflexive _≤_
    refl sym idem {x} = sym (idem x)

    antisym : IsEquivalence _≈_ → Commutative _∙_ → Antisymmetric _≈_ _≤_
    antisym isEq comm {x} {y} x≤y y≤x = begin
      x     ≈⟨ x≤y ⟩
      x ∙ y ≈⟨ comm x y ⟩
      y ∙ x ≈⟨ sym y≤x ⟩
      y     ∎
      where open IsEquivalence isEq; open ≈-Reasoning (record { isEquivalence = isEq })

    total : Symmetric _≈_ → Transitive _≈_ → Selective _∙_ → Commutative _∙_ → Total _≤_
    total sym trans sel comm x y = map sym (λ x∙y≈y → trans (sym x∙y≈y) (comm x y)) (sel x y)

    trans : IsSemigroup _∙_ → Transitive _≤_
    trans semi {x} {y} {z} x≤y y≤z = begin
      x           ≈⟨ x≤y ⟩
      x ∙ y       ≈⟨ ∙-cong S.refl y≤z ⟩
      x ∙ (y ∙ z) ≈⟨ sym (assoc x y z) ⟩
      (x ∙ y) ∙ z ≈⟨ ∙-cong (sym x≤y) S.refl ⟩
      x ∙ z       ∎
      where open module S = IsSemigroup semi; open ≈-Reasoning S.setoid

    respʳ : IsMagma _∙_ → _≤_ Respectsʳ _≈_
    respʳ magma {x} {y} {z} y≈z x≤y = begin
      x     ≈⟨ x≤y ⟩
      x ∙ y ≈⟨ ∙-cong M.refl y≈z ⟩
      x ∙ z ∎
      where open module M = IsMagma magma; open ≈-Reasoning M.setoid

    respˡ : IsMagma _∙_ → _≤_ Respectsˡ _≈_
    respˡ magma {x} {y} {z} y≈z y≤x = begin
      z     ≈⟨ sym y≈z ⟩
      y     ≈⟨ y≤x ⟩
      y ∙ x ≈⟨ ∙-cong y≈z M.refl ⟩
      z ∙ x ∎
      where open module M = IsMagma magma; open ≈-Reasoning M.setoid

    resp₂ : IsMagma _∙_ →  _≤_ Respects₂ _≈_
    resp₂ magma = respʳ magma , respˡ magma

    dec : Decidable _≈_ → Decidable _≤_
    dec _≟_ x y = x ≟ (x ∙ y)

    module _ (semi : IsSemilattice _∙_) where

      private open module S = IsSemilattice semi
      open ≈-Reasoning setoid

      x∙y≤x : ∀ x y → (x ∙ y) ≤ x
      x∙y≤x x y = begin
        x ∙ y       ≈⟨ ∙-cong (sym (idem x)) S.refl ⟩
        (x ∙ x) ∙ y ≈⟨ assoc x x y ⟩
        x ∙ (x ∙ y) ≈⟨ comm x (x ∙ y) ⟩
        (x ∙ y) ∙ x ∎

      x∙y≤y : ∀ x y → (x ∙ y) ≤ y
      x∙y≤y x y = begin
        x ∙ y        ≈⟨ ∙-cong S.refl (sym (idem y)) ⟩
        x ∙ (y ∙ y)  ≈⟨ sym (assoc x y y) ⟩
        (x ∙ y) ∙ y  ∎

      ∙-presʳ-≤ : ∀ {x y} z → z ≤ x → z ≤ y → z ≤ (x ∙ y)
      ∙-presʳ-≤ {x} {y} z z≤x z≤y = begin
        z            ≈⟨ z≤y ⟩
        z ∙ y        ≈⟨ ∙-cong z≤x S.refl ⟩
        (z ∙ x) ∙ y  ≈⟨ assoc z x y ⟩
        z ∙ (x ∙ y)  ∎

      infimum : Infimum _≤_ _∙_
      infimum x y = x∙y≤x x y , x∙y≤y x y , ∙-presʳ-≤

    ------------------------------------------------------------------------
    -- Structures

    isPreorder : IsBand _∙_ → IsPreorder _≈_ _≤_
    isPreorder band = record
      { isEquivalence = isEquivalence
      ; reflexive     = reflexive isMagma idem
      ; trans         = trans isSemigroup
      }
      where open IsBand band hiding (reflexive; trans)

    isPartialOrder : IsSemilattice _∙_ → IsPartialOrder _≈_ _≤_
    isPartialOrder semilattice = record
      { isPreorder = isPreorder isBand
      ; antisym    = antisym isEquivalence comm
      }
      where open IsSemilattice semilattice

    isDecPartialOrder : IsSemilattice _∙_ → Decidable _≈_ →
                        IsDecPartialOrder _≈_ _≤_
    isDecPartialOrder semilattice _≟_ = record
      { isPartialOrder = isPartialOrder semilattice
      ; _≟_            = _≟_
      ; _≤?_           = dec _≟_
      }

    isTotalOrder : IsSemilattice _∙_ → Selective _∙_ → IsTotalOrder _≈_ _≤_
    isTotalOrder latt sel  = record
      { isPartialOrder = isPartialOrder latt
      ; total          = total sym S.trans sel comm
      }
      where open module S = IsSemilattice latt

    isDecTotalOrder : IsSemilattice _∙_ → Selective _∙_ →
                      Decidable _≈_ → IsDecTotalOrder _≈_ _≤_
    isDecTotalOrder latt sel _≟_ = record
      { isTotalOrder = isTotalOrder latt sel
      ; _≟_          = _≟_
      ; _≤?_         = dec _≟_
      }

    ------------------------------------------------------------------------
    -- Bundles

    preorder : IsBand _∙_ → Preorder a ℓ ℓ
    preorder band = record
      { isPreorder = isPreorder band
      }

    poset : IsSemilattice _∙_ → Poset a ℓ ℓ
    poset latt = record
      { isPartialOrder = isPartialOrder latt
      }

    decPoset : IsSemilattice _∙_ → Decidable _≈_ → DecPoset a ℓ ℓ
    decPoset latt dec = record
      { isDecPartialOrder = isDecPartialOrder latt dec
      }

    totalOrder : IsSemilattice _∙_ → Selective _∙_ → TotalOrder a ℓ ℓ
    totalOrder latt sel = record
      { isTotalOrder = isTotalOrder latt sel
      }

    decTotalOrder : IsSemilattice _∙_ → Selective _∙_ →
                    Decidable _≈_ → DecTotalOrder a ℓ ℓ
    decTotalOrder latt sel dec = record
      { isDecTotalOrder = isDecTotalOrder latt sel dec
      }