From 2167866c53aa7f9cbb52e776bfb64f53acf3fa2c Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Sat, 2 Apr 2022 11:41:51 +0100 Subject: Add more properties for ordered structures. --- .../Ordered/StrictTotal/Properties/Semigroup.agda | 31 ++++++++++++++++++++++ 1 file changed, 31 insertions(+) create mode 100644 src/Helium/Algebra/Ordered/StrictTotal/Properties/Semigroup.agda (limited to 'src/Helium/Algebra/Ordered/StrictTotal/Properties/Semigroup.agda') 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 -- cgit v1.2.3