------------------------------------------------------------------------ -- The Agda standard library -- -- Basic definition of an operator that computes the min/max value -- with respect to a total ordering. ------------------------------------------------------------------------ {-# OPTIONS --without-K --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 7 _⊓_ 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 6 _⊔_ 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