------------------------------------------------------------------------
-- The Agda standard library
--
-- The min operator derived from an arbitrary total preorder.
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
open import Relation.Binary.Bundles using (TotalOrder)
 
module Algebra.Construct.NaturalChoice.Min
  {a ℓ₁ ℓ₂} (O : TotalOrder a ℓ₁ ℓ₂)
  where
 
open import Algebra.Core using (Op₂)
open import Algebra.Construct.NaturalChoice.Base
import Algebra.Construct.NaturalChoice.MinOp as MinOp
open import Data.Sum.Base using (inj₁; inj₂; [_,_])
open import Data.Product.Base using (_,_)
open import Function.Base using (id)
open TotalOrder O renaming (Carrier to A)
 
------------------------------------------------------------------------
-- Definition
 
infixl  _⊓_
 
_⊓_ : Op₂ A
x ⊓ y with total x y
... | inj₁ x≤y = x
... | inj₂ y≤x = y
 
------------------------------------------------------------------------
-- Properties
 
x≤y⇒x⊓y≈x : ∀ {x y} → x ≤ y → x ⊓ y ≈ x
x≤y⇒x⊓y≈x {x} {y} x≤y with total x y
... | inj₁ _   = Eq.refl
... | inj₂ y≤x = antisym y≤x x≤y
 
x≤y⇒y⊓x≈x : ∀ {x y} → x ≤ y → y ⊓ x ≈ x
x≤y⇒y⊓x≈x {x} {y} x≤y with total y x
... | inj₁ y≤x = antisym y≤x x≤y
... | inj₂ _   = Eq.refl
 
minOperator : MinOperator totalPreorder
minOperator = record
  { x≤y⇒x⊓y≈x = x≤y⇒x⊓y≈x
  ; x≥y⇒x⊓y≈y = x≤y⇒y⊓x≈x
  }
 
open MinOp minOperator public