```------------------------------------------------------------------------
-- The Agda standard library
--
-- Basic definition of an operator that computes the min/max value
-- with respect to a total preorder.
------------------------------------------------------------------------

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

open import Algebra.Core
open import Level as L hiding (_⊔_)
open import Function.Base using (flip)
open import Relation.Binary.Bundles using (TotalPreorder)
open import Relation.Binary.Construct.Flip.EqAndOrd using ()
renaming (totalPreorder to flipOrder)
import Relation.Binary.Properties.TotalOrder as TotalOrderProperties

module Algebra.Construct.NaturalChoice.Base where

private
variable
a ℓ₁ ℓ₂ : Level
O : TotalPreorder a ℓ₁ ℓ₂

------------------------------------------------------------------------
-- Definition

module _ (O : TotalPreorder a ℓ₁ ℓ₂) where
open TotalPreorder O renaming (_≲_ to _≤_)
private _≥_ = flip _≤_

record MinOperator : Set (a L.⊔ ℓ₁ L.⊔ ℓ₂) where
infixl 7 _⊓_
field
_⊓_       : Op₂ Carrier
x≤y⇒x⊓y≈x : ∀ {x y} → x ≤ y → x ⊓ y ≈ x
x≥y⇒x⊓y≈y : ∀ {x y} → x ≥ y → x ⊓ y ≈ y

record MaxOperator : Set (a L.⊔ ℓ₁ L.⊔ ℓ₂) where
infixl 6 _⊔_
field
_⊔_       : Op₂ Carrier
x≤y⇒x⊔y≈y : ∀ {x y} → x ≤ y → x ⊔ y ≈ y
x≥y⇒x⊔y≈x : ∀ {x y} → x ≥ y → x ⊔ y ≈ x

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

MinOp⇒MaxOp : MinOperator O → MaxOperator (flipOrder O)
MinOp⇒MaxOp minOp = record
{ _⊔_       = _⊓_
; x≤y⇒x⊔y≈y = x≥y⇒x⊓y≈y
; x≥y⇒x⊔y≈x = x≤y⇒x⊓y≈x
} where open MinOperator minOp

MaxOp⇒MinOp : MaxOperator O → MinOperator (flipOrder O)
MaxOp⇒MinOp maxOp = record
{ _⊓_       = _⊔_
; x≤y⇒x⊓y≈x = x≥y⇒x⊔y≈x
; x≥y⇒x⊓y≈y = x≤y⇒x⊔y≈y
} where open MaxOperator maxOp
```