Add some required algebraic types.

1 files changed, 48 insertions, 0 deletions

diff --git a/src/Helium/Algebra/Consequences/Setoid.agda b/src/Helium/Algebra/Consequences/Setoid.agda
new file mode 100644
index 0000000..ab8d41e
--- /dev/null
+++ b/src/Helium/Algebra/Consequences/Setoid.agda
@@ -0,0 +1,48 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Relations between properties of functions when the underlying relation is a setoid
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary using (Setoid)
+
+module Helium.Algebra.Consequences.Setoid {a ℓ} (S : Setoid a ℓ) where
+
+open Setoid S renaming (Carrier to A)
+open import Algebra.Core
+open import Algebra.Definitions _≈_
+open import Data.Product using (_,_)
+open import Helium.Algebra.Core
+open import Helium.Algebra.Definitions _≈_
+open import Relation.Nullary using (¬_)
+
+open import Relation.Binary.Reasoning.Setoid S
+
+module _ {0# 1#} {_∙_ : Op₂ A} {_⁻¹ : AlmostOp₁ _≈_ 0#} (cong : Congruent₂ _∙_) where
+  assoc+id+invʳ⇒invˡ-unique : Associative _∙_ →
+                              Identity 1# _∙_ →
+                              AlmostRightInverse 1# _⁻¹ _∙_ →
+                              ∀ x {y} (y≉0 : ¬ y ≈ 0#) →
+                              (x ∙ y) ≈ 1# → x ≈ (y≉0 ⁻¹)
+  assoc+id+invʳ⇒invˡ-unique assoc (idˡ , idʳ) invʳ x {y} y≉0 eq = begin
+    x                  ≈˘⟨ idʳ x ⟩
+    x ∙ 1#             ≈˘⟨ cong refl (invʳ y≉0) ⟩
+    x ∙ (y ∙ (y≉0 ⁻¹)) ≈˘⟨ assoc x y (y≉0 ⁻¹) ⟩
+    (x ∙ y) ∙ (y≉0 ⁻¹) ≈⟨  cong eq refl ⟩
+    1# ∙ (y≉0 ⁻¹)      ≈⟨  idˡ (y≉0 ⁻¹) ⟩
+    y≉0 ⁻¹             ∎
+
+  assoc+id+invˡ⇒invʳ-unique : Associative _∙_ →
+                              Identity 1# _∙_ →
+                              AlmostLeftInverse 1# _⁻¹ _∙_ →
+                              ∀ {x} (x≉0 : ¬ x ≈ 0#)  y →
+                              (x ∙ y) ≈ 1# → y ≈ (x≉0 ⁻¹)
+  assoc+id+invˡ⇒invʳ-unique assoc (idˡ , idʳ) invˡ {x} x≉0 y eq = begin
+    y                  ≈˘⟨ idˡ y ⟩
+    1# ∙ y             ≈˘⟨ cong (invˡ x≉0) refl ⟩
+    ((x≉0 ⁻¹) ∙ x) ∙ y ≈⟨  assoc (x≉0 ⁻¹) x y ⟩
+    (x≉0 ⁻¹) ∙ (x ∙ y) ≈⟨  cong refl eq ⟩
+    (x≉0 ⁻¹) ∙ 1#      ≈⟨  idʳ (x≉0 ⁻¹) ⟩
+    x≉0 ⁻¹             ∎