Define ordered algebraic structures.

1 files changed, 29 insertions, 0 deletions

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)