    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Properties of a min operator derived from a spec over a total
    -- preorder.
    ------------------------------------------------------------------------

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

    open import Algebra.Construct.NaturalChoice.Base using (MinOperator)
    open import Relation.Binary.Bundles using (TotalPreorder)

    module Algebra.Lattice.Construct.NaturalChoice.MinOp
      {a ℓ₁ ℓ₂} {O : TotalPreorder a ℓ₁ ℓ₂} (minOp : MinOperator O) where

    open TotalPreorder O
    open MinOperator minOp

    open import Algebra.Construct.NaturalChoice.MinOp minOp
    open import Algebra.Lattice.Bundles using (Semilattice)
    open import Algebra.Lattice.Structures _≈_

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

    ⊓-isSemilattice : IsSemilattice _⊓_
    ⊓-isSemilattice = record
      { isBand = ⊓-isBand
      ; comm   = ⊓-comm
      }

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

    ⊓-semilattice : Semilattice _ _
    ⊓-semilattice = record
      { isSemilattice = ⊓-isSemilattice
      }