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

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

open import Algebra.Core
open import Level as L hiding (_⊔_)
open import Function.Base using (flip)
open import Relation.Binary
open import Relation.Binary.Construct.Converse 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