    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- The max operator derived from an arbitrary total preorder.
    ------------------------------------------------------------------------

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

    open import Relation.Binary.Bundles using (TotalOrder)

    module Algebra.Construct.NaturalChoice.Max
      {a ℓ₁ ℓ₂} (totalOrder : TotalOrder a ℓ₁ ℓ₂) where

    open import Algebra.Core using (Op₂)
    open import Algebra.Construct.NaturalChoice.Base using (MaxOperator)
    open import Relation.Binary.Construct.Flip.EqAndOrd using ()
      renaming (totalOrder to flip)

    open TotalOrder totalOrder renaming (Carrier to A)

    ------------------------------------------------------------------------
    -- Max is just min with a flipped order

    import Algebra.Construct.NaturalChoice.Min (flip totalOrder) as Min

    infixl 6 _⊔_

    _⊔_ : Op₂ A
    _⊔_ = Min._⊓_

    ------------------------------------------------------------------------
    -- Properties

    open Min public using ()
      renaming
      ( x≤y⇒x⊓y≈x to x≤y⇒y⊔x≈y
      ; x≤y⇒y⊓x≈x to x≤y⇒x⊔y≈y
      )

    maxOperator : MaxOperator totalPreorder
    maxOperator = record
      { x≤y⇒x⊔y≈y = x≤y⇒x⊔y≈y
      ; x≥y⇒x⊔y≈x = x≤y⇒y⊔x≈y
      }

    open import Algebra.Construct.NaturalChoice.MaxOp maxOperator public