    ------------------------------------------------------------------------
    -- 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.Construct.NaturalChoice.MaxOp
      {a ℓ₁ ℓ₂} {O : TotalPreorder a ℓ₁ ℓ₂} (maxOp : MaxOperator O)
      where

    import Algebra.Construct.NaturalChoice.MinOp as MinOp
    open import Algebra.Core using (Op₂)
    open import Function.Base using (flip)
    open MaxOperator maxOp
    open import Relation.Binary.Core using (_Preserves_⟶_)
    open import Relation.Binary.Construct.Flip.EqAndOrd using ()
      renaming (totalPreorder to flipOrder)
    open TotalPreorder O renaming (Carrier to A; _≲_ to _≤_)

    -- Max is just min with a flipped order

    private
      module Min = MinOp (MaxOp⇒MinOp maxOp)

    open Min public
      using ()
      renaming
      ( ⊓-cong       to  ⊔-cong
      ; ⊓-congʳ      to  ⊔-congʳ
      ; ⊓-congˡ      to  ⊔-congˡ
      ; ⊓-idem       to  ⊔-idem
      ; ⊓-sel        to  ⊔-sel
      ; ⊓-assoc      to  ⊔-assoc
      ; ⊓-comm       to  ⊔-comm

      ; ⊓-identityˡ  to  ⊔-identityˡ
      ; ⊓-identityʳ  to  ⊔-identityʳ
      ; ⊓-identity   to  ⊔-identity
      ; ⊓-zeroˡ      to  ⊔-zeroˡ
      ; ⊓-zeroʳ      to  ⊔-zeroʳ
      ; ⊓-zero       to  ⊔-zero

      ; ⊓-isMagma                 to  ⊔-isMagma
      ; ⊓-isSemigroup             to  ⊔-isSemigroup
      ; ⊓-isCommutativeSemigroup  to  ⊔-isCommutativeSemigroup
      ; ⊓-isBand                  to  ⊔-isBand
      ; ⊓-isMonoid                to  ⊔-isMonoid
      ; ⊓-isSelectiveMagma        to  ⊔-isSelectiveMagma

      ; ⊓-magma                   to  ⊔-magma
      ; ⊓-semigroup               to  ⊔-semigroup
      ; ⊓-commutativeSemigroup    to  ⊔-commutativeSemigroup
      ; ⊓-band                    to  ⊔-band
      ; ⊓-monoid                  to  ⊔-monoid
      ; ⊓-selectiveMagma          to  ⊔-selectiveMagma

      ; x⊓y≈y⇒y≤x  to x⊔y≈y⇒x≤y
      ; x⊓y≈x⇒x≤y  to x⊔y≈x⇒y≤x
      ; x⊓y≤x      to x≤x⊔y
      ; x⊓y≤y      to x≤y⊔x
      ; x≤y⇒x⊓z≤y  to x≤y⇒x≤y⊔z
      ; x≤y⇒z⊓x≤y  to x≤y⇒x≤z⊔y
      ; x≤y⊓z⇒x≤y  to x⊔y≤z⇒x≤z
      ; x≤y⊓z⇒x≤z  to x⊔y≤z⇒y≤z

      ; ⊓-glb              to  ⊔-lub
      ; ⊓-triangulate      to  ⊔-triangulate
      ; ⊓-mono-≤           to  ⊔-mono-≤
      ; ⊓-monoˡ-≤          to  ⊔-monoˡ-≤
      ; ⊓-monoʳ-≤          to  ⊔-monoʳ-≤
      )

    mono-≤-distrib-⊔ : ∀ {f} → f Preserves _≈_ ⟶ _≈_ → f Preserves _≤_ ⟶ _≤_ →
                       ∀ x y → f (x ⊔ y) ≈ f x ⊔ f y
    mono-≤-distrib-⊔ cong pres = Min.mono-≤-distrib-⊓ cong pres