From 1f718c9dbe48934edf115aef285c5aeaa2dfb20d Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Fri, 7 Jan 2022 13:36:42 +0000 Subject: Add some required algebraic types. --- src/Helium/Algebra/Definitions.agda | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) create mode 100644 src/Helium/Algebra/Definitions.agda (limited to 'src/Helium/Algebra/Definitions.agda') 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 ⁻¹ ∙ -- cgit v1.2.3