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

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

    open import Algebra.Construct.NaturalChoice.Base
      using (MaxOperator; MaxOp⇒MinOp)
    open import Relation.Binary.Bundles using (TotalPreorder)

    module Algebra.Lattice.Construct.NaturalChoice.MaxOp
      {a ℓ₁ ℓ₂} {O : TotalPreorder a ℓ₁ ℓ₂} (maxOp : MaxOperator O)
      where

    import Algebra.Lattice.Construct.NaturalChoice.MinOp as MinOp

    private
      module Min = MinOp (MaxOp⇒MinOp maxOp)

    open Min public
      using ()
      renaming
      ( ⊓-isSemilattice           to  ⊔-isSemilattice
      ; ⊓-semilattice             to  ⊔-semilattice
      )