------------------------------------------------------------------------
-- The Agda standard library
--
-- The max operator derived from an arbitrary total preorder.
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Relation.Binary.Bundles using (TotalOrder)
module Algebra.Construct.NaturalChoice.Max
{a ℓ₁ ℓ₂} (totalOrder : TotalOrder a ℓ₁ ℓ₂) where
open import Algebra.Core using (Op₂)
open import Algebra.Construct.NaturalChoice.Base using (MaxOperator)
open import Relation.Binary.Construct.Flip.EqAndOrd using ()
renaming (totalOrder to flip)
open TotalOrder totalOrder renaming (Carrier to A)
------------------------------------------------------------------------
-- Max is just min with a flipped order
import Algebra.Construct.NaturalChoice.Min (flip totalOrder) as Min
infixl 6 _⊔_
_⊔_ : Op₂ A
_⊔_ = Min._⊓_
------------------------------------------------------------------------
-- Properties
open Min public using ()
renaming
( x≤y⇒x⊓y≈x to x≤y⇒y⊔x≈y
; x≤y⇒y⊓x≈x to x≤y⇒x⊔y≈y
)
maxOperator : MaxOperator totalPreorder
maxOperator = record
{ x≤y⇒x⊔y≈y = x≤y⇒x⊔y≈y
; x≥y⇒x⊔y≈x = x≤y⇒y⊔x≈y
}
open import Algebra.Construct.NaturalChoice.MaxOp maxOperator 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