1 files changed, 31 insertions, 0 deletions
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Semigroup.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Semigroup.agda
new file mode 100644
index 0000000..17228ac
--- /dev/null
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Semigroup.agda
@@ -0,0 +1,31 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Algebraic properties of ordered semigroups
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+open import Helium.Algebra.Ordered.StrictTotal.Bundles
+
+module Helium.Algebra.Ordered.StrictTotal.Properties.Semigroup
+  {ℓ₁ ℓ₂ ℓ₃}
+  (semigroup : Semigroup ℓ₁ ℓ₂ ℓ₃)
+  where
+
+open Semigroup semigroup
+  renaming
+  ( trans to <-trans
+  ; irrefl to <-irrefl
+  ; asym to <-asym
+  )
+
+open import Helium.Algebra.Ordered.StrictTotal.Properties.Magma magma public
+  using
+  ( ∙-mono-<; ∙-monoˡ-<; ∙-monoʳ-<
+  ; ∙-mono-≤; ∙-monoˡ-≤; ∙-monoʳ-≤
+  ; ∙-cancelˡ; ∙-cancelʳ; ∙-cancel
+  ; ∙-cancelˡ-<; ∙-cancelʳ-<; ∙-cancel-<
+  ; ∙-cancelˡ-≤; ∙-cancelʳ-≤; ∙-cancel-≤
+  )
+open import Helium.Relation.Binary.Properties.StrictTotalOrder strictTotalOrder public