Add some required algebraic types.

1 files changed, 32 insertions, 0 deletions

diff --git a/src/Helium/Algebra/Definitions.agda b/src/Helium/Algebra/Definitions.agda
new file mode 100644
index 0000000..217b353
--- /dev/null
+++ b/src/Helium/Algebra/Definitions.agda
@@ -0,0 +1,32 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- More properties of functions
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary.Core using (Rel)
+
+module Helium.Algebra.Definitions
+  {a ℓ} {A : Set a} -- The underlying set
+  (_≈_ : Rel A ℓ)   -- The underlying equality
+  where
+
+open import Algebra.Core
+open import Data.Product using (_×_)
+open import Helium.Algebra.Core
+open import Relation.Nullary using (¬_)
+
+AlmostCongruent₁ : ∀ {ε} → AlmostOp₁ _≈_ ε → Set _
+AlmostCongruent₁ {ε} f =
+  ∀ {x y} {x≉ε : ¬ x ≈ ε} {y≉ε : ¬ y ≈ ε} → x ≈ y → f x≉ε ≈ f y≉ε
+
+AlmostLeftInverse : ∀ {ε} → A → AlmostOp₁ _≈_ ε → Op₂ A → Set _
+AlmostLeftInverse {ε} e _⁻¹ _∙_ = ∀ {x} (x≉ε : ¬ x ≈ ε) → ((x≉ε ⁻¹) ∙ x) ≈ e
+
+AlmostRightInverse : ∀ {ε} → A → AlmostOp₁ _≈_ ε → Op₂ A → Set _
+AlmostRightInverse {ε} e _⁻¹ _∙_ = ∀ {x} (x≉ε : ¬ x ≈ ε) → (x ∙ (x≉ε ⁻¹)) ≈ e
+
+AlmostInverse : ∀ {ε} → A → AlmostOp₁ _≈_ ε → Op₂ A → Set _
+AlmostInverse e ⁻¹ ∙ = AlmostLeftInverse e ⁻¹ ∙ × AlmostRightInverse e ⁻¹ ∙