    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Properties satisfied by bounded meet semilattices
    ------------------------------------------------------------------------

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

    open import Relation.Binary.Lattice
      using (BoundedMeetSemilattice; IsBoundedJoinSemilattice; BoundedJoinSemilattice)

    module Relation.Binary.Lattice.Properties.BoundedMeetSemilattice
      {c ℓ₁ ℓ₂} (M : BoundedMeetSemilattice c ℓ₁ ℓ₂) where

    open import Function.Base using (_∘_; flip)

    open BoundedMeetSemilattice M
      using (⊤; _∧_; isBoundedMeetSemilattice; _≈_; poset; _≤_; infimum; maximum)

    open import Algebra.Definitions _≈_
      using (LeftIdentity; RightIdentity; Identity)
    open import Relation.Binary.Properties.Poset poset using (≥-isPartialOrder)
    import Relation.Binary.Lattice.Properties.BoundedJoinSemilattice as J

    -- The dual construction is a bounded join semilattice.

    dualIsBoundedJoinSemilattice : IsBoundedJoinSemilattice _≈_ (flip _≤_) _∧_ ⊤
    dualIsBoundedJoinSemilattice = record
      { isJoinSemilattice = record
        { isPartialOrder  = ≥-isPartialOrder
        ; supremum        = infimum
        }
      ; minimum           = maximum
      }

    dualBoundedJoinSemilattice : BoundedJoinSemilattice c ℓ₁ ℓ₂
    dualBoundedJoinSemilattice = record
      { ⊥                        = ⊤
      ; isBoundedJoinSemilattice = dualIsBoundedJoinSemilattice
      }

    open J dualBoundedJoinSemilattice
      hiding (dualIsBoundedMeetSemilattice; dualBoundedMeetSemilattice) public