------------------------------------------------------------------------
-- 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 7 _⊓_
_⊓_ : 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
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4