------------------------------------------------------------------------
-- 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 using (Op₂)
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  _⊓_
    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  _⊔_
    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