    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Some derivable properties of semilattices
    ------------------------------------------------------------------------

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

    open import Algebra.Lattice.Bundles using (Semilattice)

    module Algebra.Lattice.Properties.Semilattice
      {c ℓ} (L : Semilattice c ℓ) where

    open import Relation.Binary.Bundles using (Poset)
    import Relation.Binary.Lattice as B
    import Relation.Binary.Properties.Poset as PosetProperties
    open Semilattice L renaming (_∙_ to _∧_)

    open import Relation.Binary.Reasoning.Setoid setoid
    import Relation.Binary.Construct.NaturalOrder.Left _≈_ _∧_
      as LeftNaturalOrder

    ------------------------------------------------------------------------
    -- Every semilattice can be turned into a poset via the left natural
    -- order.

    poset : Poset c ℓ ℓ
    poset = LeftNaturalOrder.poset isSemilattice

    open Poset poset using (_≤_; _≥_; isPartialOrder)
    open PosetProperties poset using (≥-isPartialOrder)

    ------------------------------------------------------------------------
    -- Every algebraic semilattice can be turned into an order-theoretic one.

    ∧-isOrderTheoreticMeetSemilattice : B.IsMeetSemilattice _≈_ _≤_ _∧_
    ∧-isOrderTheoreticMeetSemilattice = record
      { isPartialOrder = isPartialOrder
      ; infimum        = LeftNaturalOrder.infimum isSemilattice
      }

    ∧-isOrderTheoreticJoinSemilattice : B.IsJoinSemilattice _≈_ _≥_ _∧_
    ∧-isOrderTheoreticJoinSemilattice = record
      { isPartialOrder = ≥-isPartialOrder
      ; supremum       = B.IsMeetSemilattice.infimum
                           ∧-isOrderTheoreticMeetSemilattice
      }

    ∧-orderTheoreticMeetSemilattice : B.MeetSemilattice c ℓ ℓ
    ∧-orderTheoreticMeetSemilattice = record
      { isMeetSemilattice = ∧-isOrderTheoreticMeetSemilattice
      }

    ∧-orderTheoreticJoinSemilattice : B.JoinSemilattice c ℓ ℓ
    ∧-orderTheoreticJoinSemilattice = record
      { isJoinSemilattice = ∧-isOrderTheoreticJoinSemilattice
      }