From f640cb65e9106be5674f8f13d9594d12966d823a Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Sun, 16 Jan 2022 16:59:55 +0000 Subject: Define ordered algebraic structures. --- src/Helium/Algebra/Ordered/Definitions.agda | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) create mode 100644 src/Helium/Algebra/Ordered/Definitions.agda (limited to 'src/Helium/Algebra/Ordered/Definitions.agda') diff --git a/src/Helium/Algebra/Ordered/Definitions.agda b/src/Helium/Algebra/Ordered/Definitions.agda new file mode 100644 index 0000000..4ac1070 --- /dev/null +++ b/src/Helium/Algebra/Ordered/Definitions.agda @@ -0,0 +1,29 @@ +------------------------------------------------------------------------ +-- Agda Helium +-- +-- Ordering properties of functions +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +open import Relation.Binary.Core using (Rel) + +module Helium.Algebra.Ordered.Definitions + {a ℓ} {A : Set a} -- The underlying set + (_≤_ : Rel A ℓ) -- The underlying order + where + +open import Algebra.Core +open import Data.Product using (_×_) + +LeftInvariant : Op₂ A → Set _ +LeftInvariant _∙_ = ∀ {x y} z → x ≤ y → (z ∙ x) ≤ (z ∙ y) + +RightInvariant : Op₂ A → Set _ +RightInvariant _∙_ = ∀ {x y} z → x ≤ y → (x ∙ z) ≤ (y ∙ z) + +Invariant : Op₂ A → Set _ +Invariant ∙ = LeftInvariant ∙ × RightInvariant ∙ + +PreservesPositive : A → Op₂ A → Set _ +PreservesPositive 0# _∙_ = ∀ {x y} → 0# ≤ x → 0# ≤ y → 0# ≤ (x ∙ y) -- cgit v1.2.3