Add more properties for ordered structures.

1 files changed, 89 insertions, 0 deletions

diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Magma.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Magma.agda
new file mode 100644
index 0000000..91d4b3e
--- /dev/null
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Magma.agda
@@ -0,0 +1,89 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Algebraic properties of ordered magmas
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+open import Helium.Algebra.Ordered.StrictTotal.Bundles
+
+module Helium.Algebra.Ordered.StrictTotal.Properties.Magma
+  {ℓ₁ ℓ₂ ℓ₃}
+  (magma : Magma ℓ₁ ℓ₂ ℓ₃)
+  where
+
+open Magma magma
+  renaming
+  ( trans to <-trans
+  ; irrefl to <-irrefl
+  ; asym to <-asym
+  )
+
+open import Algebra.Definitions
+open import Data.Product using (_,_)
+open import Helium.Algebra.Ordered.StrictTotal.Consequences strictTotalOrder
+
+open import Helium.Relation.Binary.Properties.StrictTotalOrder strictTotalOrder public
+
+--------------------------------------------------------------------------------
+-- Properties of _∙_
+
+---- Congruences
+
+-- _<_
+
+∙-mono-< : Congruent₂ _<_ _∙_
+∙-mono-< = invariant⇒mono-< ∙-invariant
+
+∙-monoˡ-< : LeftCongruent _<_ _∙_
+∙-monoˡ-< = invariantˡ⇒monoˡ-< ∙-invariantˡ
+
+∙-monoʳ-< : RightCongruent _<_ _∙_
+∙-monoʳ-< = invariantʳ⇒monoʳ-< ∙-invariantʳ
+
+-- _≤_
+
+∙-mono-≤ : Congruent₂ _≤_ _∙_
+∙-mono-≤ = cong+invariant⇒mono-≤ ∙-cong ∙-invariant
+
+∙-monoˡ-≤ : LeftCongruent _≤_ _∙_
+∙-monoˡ-≤ {x} = congˡ+monoˡ-<⇒monoˡ-≤ (∙-congˡ {x}) (∙-monoˡ-< {x}) {x}
+
+∙-monoʳ-≤ : RightCongruent _≤_ _∙_
+∙-monoʳ-≤ {x} = congʳ+monoʳ-<⇒monoʳ-≤ (∙-congʳ {x}) (∙-monoʳ-< {x}) {x}
+
+---- Cancelling
+
+-- _≈_
+
+∙-cancelˡ : LeftCancellative _≈_ _∙_
+∙-cancelˡ = monoˡ-<⇒cancelˡ ∙-monoˡ-<
+
+∙-cancelʳ : RightCancellative _≈_ _∙_
+∙-cancelʳ {x} = monoʳ-<⇒cancelʳ (∙-monoʳ-< {x}) {x}
+
+∙-cancel : Cancellative _≈_ _∙_
+∙-cancel = ∙-cancelˡ , ∙-cancelʳ
+
+-- _<_
+
+∙-cancelˡ-< : LeftCancellative _<_ _∙_
+∙-cancelˡ-< = monoˡ-≤⇒cancelˡ-< ∙-monoˡ-≤
+
+∙-cancelʳ-< : RightCancellative _<_ _∙_
+∙-cancelʳ-< {x} = monoʳ-≤⇒cancelʳ-< (∙-monoʳ-≤ {x}) {x}
+
+∙-cancel-< : Cancellative _<_ _∙_
+∙-cancel-< = ∙-cancelˡ-< , ∙-cancelʳ-<
+
+-- _≤_
+
+∙-cancelˡ-≤ : LeftCancellative _≤_ _∙_
+∙-cancelˡ-≤ = monoˡ-<⇒cancelˡ-≤ ∙-monoˡ-<
+
+∙-cancelʳ-≤ : RightCancellative _≤_ _∙_
+∙-cancelʳ-≤ {x} = monoʳ-<⇒cancelʳ-≤ (∙-monoʳ-< {x}) {x}
+
+∙-cancel-≤ : Cancellative _≤_ _∙_
+∙-cancel-≤ = ∙-cancelˡ-≤ , ∙-cancelʳ-≤