Add some required algebraic types.

5 files changed, 511 insertions, 0 deletions

diff --git a/src/Helium/Algebra/Bundles.agda b/src/Helium/Algebra/Bundles.agda
new file mode 100644
index 0000000..06a0bf2
--- /dev/null
+++ b/src/Helium/Algebra/Bundles.agda
@@ -0,0 +1,250 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Definitions for more algebraic structures
+-- (packed in records together with sets, operations, etc.)
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+module Helium.Algebra.Bundles where
+
+open import Algebra.Bundles
+open import Algebra.Core
+open import Helium.Algebra.Core
+open import Helium.Algebra.Structures
+open import Level using (_⊔_; suc)
+open import Relation.Binary.Core using (Rel)
+
+record RawAlmostGroup c ℓ : Set (suc (c ⊔ ℓ)) where
+  infix 8 _⁻¹
+  infixl 7 _∙_
+  infixl 6 _-_
+  infix 4 _≈_
+  field
+    Carrier : Set c
+    _≈_     : Rel Carrier ℓ
+    _∙_     : Op₂ Carrier
+    0#      : Carrier
+    1#      : Carrier
+    _⁻¹     : AlmostOp₁ _≈_ 0#
+
+  _-_ : AlmostOp₂ _≈_ 0#
+  x - y≉0 = x ∙ y≉0 ⁻¹
+
+  rawMonoid : RawMonoid c ℓ
+  rawMonoid = record
+    { _≈_ = _≈_
+    ; _∙_ = _∙_
+    ; ε = 1#
+    }
+
+  open RawMonoid rawMonoid public
+    using (_≉_; rawMagma)
+
+record AlmostGroup c ℓ : Set (suc (c ⊔ ℓ)) where
+  infix  8 _⁻¹
+  infixl 7 _∙_
+  infix  4 _≈_
+  field
+    Carrier       : Set c
+    _≈_           : Rel Carrier ℓ
+    _∙_           : Op₂ Carrier
+    0#            : Carrier
+    1#            : Carrier
+    _⁻¹           : AlmostOp₁ _≈_ 0#
+    isAlmostGroup : IsAlmostGroup _≈_ _∙_ 0# 1# _⁻¹
+
+  open IsAlmostGroup isAlmostGroup public
+
+  rawAlmostGroup : RawAlmostGroup _ _
+  rawAlmostGroup = record
+    { _≈_ = _≈_
+    ; _∙_ = _∙_
+    ; 0# = 0#
+    ; 1# = 1#
+    ; _⁻¹ = _⁻¹
+    }
+
+  monoid : Monoid _ _
+  monoid = record { isMonoid = isMonoid }
+
+  open Monoid monoid public
+    using (_≉_; rawMagma; magma; semigroup; rawMonoid)
+
+record AlmostAbelianGroup c ℓ : Set (suc (c ⊔ ℓ)) where
+  infix  8 _⁻¹
+  infixl 7 _∙_
+  infix  4 _≈_
+  field
+    Carrier              : Set c
+    _≈_                  : Rel Carrier ℓ
+    _∙_                  : Op₂ Carrier
+    0#                   : Carrier
+    1#                   : Carrier
+    _⁻¹                  : AlmostOp₁ _≈_ 0#
+    isAlmostAbelianGroup : IsAlmostAbelianGroup _≈_ _∙_ 0# 1# _⁻¹
+
+  open IsAlmostAbelianGroup isAlmostAbelianGroup public
+
+  almostGroup : AlmostGroup _ _
+  almostGroup = record { isAlmostGroup = isAlmostGroup }
+
+  open AlmostGroup almostGroup public
+    using (_≉_; rawMagma; magma; semigroup; monoid; rawMonoid; rawAlmostGroup)
+
+  commutativeMonoid : CommutativeMonoid _ _
+  commutativeMonoid = record { isCommutativeMonoid = isCommutativeMonoid }
+
+  open CommutativeMonoid commutativeMonoid public
+    using (commutativeMagma; commutativeSemigroup)
+
+record RawField c ℓ : Set (suc (c ⊔ ℓ)) where
+  infix  9 _⁻¹
+  infix  8 -_
+  infixl 7 _*_ _/_
+  infixl 6 _+_ _-_
+  infix  4 _≈_
+  field
+    Carrier : Set c
+    _≈_     : Rel Carrier ℓ
+    _+_     : Op₂ Carrier
+    _*_     : Op₂ Carrier
+    -_      : Op₁ Carrier
+    0#      : Carrier
+    1#      : Carrier
+    _⁻¹     : AlmostOp₁ _≈_ 0#
+
+  rawRing : RawRing c ℓ
+  rawRing = record
+    { _≈_ = _≈_
+    ; _+_ = _+_
+    ; _*_ = _*_
+    ; -_ = -_
+    ; 0# = 0#
+    ; 1# = 1#
+    }
+
+  open RawRing rawRing public
+    using
+    ( _≉_
+    ; +-rawMagma; +-rawMonoid; +-rawGroup
+    ; *-rawMagma; *-rawMonoid
+    ; rawSemiring
+    )
+
+  *-rawAlmostGroup : RawAlmostGroup _ _
+  *-rawAlmostGroup = record
+                       { _≈_ = _≈_ ; _∙_ = _*_ ; 0# = 0# ; 1# = 1# ; _⁻¹ = _⁻¹ }
+
+  _-_ : Op₂ Carrier
+  x - y = x + - y
+
+  _/_ : AlmostOp₂ _≈_ 0#
+  x / y≉0 = x * y≉0 ⁻¹
+
+record DivisionRing c ℓ : Set (suc (c ⊔ ℓ)) where
+  infix  9 _⁻¹
+  infix  8 -_
+  infixl 7 _*_
+  infixl 6 _+_
+  infix  4 _≈_
+  field
+    Carrier        : Set c
+    _≈_            : Rel Carrier ℓ
+    _+_            : Op₂ Carrier
+    _*_            : Op₂ Carrier
+    -_             : Op₁ Carrier
+    0#             : Carrier
+    1#             : Carrier
+    _⁻¹            : AlmostOp₁ _≈_ 0#
+    isDivisionRing : IsDivisionRing _≈_ _+_ _*_ -_ 0# 1# _⁻¹
+
+  open IsDivisionRing isDivisionRing public
+
+  ring : Ring _ _
+  ring = record
+    { _≈_ = _≈_
+    ; _+_ = _+_
+    ; _*_ = _*_
+    ; -_ = -_
+    ; 0# = 0#
+    ; 1# = 1#
+    ; isRing = isRing
+    }
+
+  open Ring ring public
+    using
+    ( _≉_
+    ; +-rawMagma; +-magma; +-commutativeMagma
+    ; +-semigroup; +-commutativeSemigroup
+    ; +-rawMonoid; +-monoid; +-commutativeMonoid
+    ; +-group; +-abelianGroup
+    ; *-rawMagma; *-magma ; *-semigroup; *-rawMonoid; *-monoid
+    ; nearSemiring ; semiringWithoutOne; semiringWithoutAnnihilatingZero
+    ; semiring
+    ; rawRing
+    )
+
+  rawField : RawField _ _
+  rawField = record
+    { _≈_ = _≈_
+    ; _+_ = _+_
+    ; _*_ = _*_
+    ; -_ = -_
+    ; 0# = 0#
+    ; 1# = 1#
+    ; _⁻¹ = _⁻¹
+    }
+
+  open RawField rawField public
+    using (+-rawGroup; *-rawAlmostGroup; rawSemiring)
+
+  *-almostGroup : AlmostGroup _ _
+  *-almostGroup = record { isAlmostGroup = *-isAlmostGroup }
+
+record Field c ℓ : Set (suc (c ⊔ ℓ)) where
+  infix  9 _⁻¹
+  infix  8 -_
+  infixl 7 _*_
+  infixl 6 _+_
+  infix  4 _≈_
+  field
+    Carrier : Set c
+    _≈_     : Rel Carrier ℓ
+    _+_     : Op₂ Carrier
+    _*_     : Op₂ Carrier
+    -_      : Op₁ Carrier
+    0#      : Carrier
+    1#      : Carrier
+    _⁻¹     : AlmostOp₁ _≈_ 0#
+    isField : IsField _≈_ _+_ _*_ -_ 0# 1# _⁻¹
+
+  open IsField isField public
+
+  divisionRing : DivisionRing _ _
+  divisionRing = record { isDivisionRing = isDivisionRing }
+
+  open DivisionRing divisionRing public
+    using
+    ( _≉_
+    ; +-rawMagma; +-magma; +-commutativeMagma
+    ; +-semigroup; +-commutativeSemigroup
+    ; +-rawMonoid; +-monoid; +-commutativeMonoid
+    ; +-rawGroup; +-group; +-abelianGroup
+    ; *-rawMagma; *-magma ; *-semigroup
+    ; *-rawMonoid; *-monoid
+    ; *-rawAlmostGroup; *-almostGroup
+    ; nearSemiring ; semiringWithoutOne; semiringWithoutAnnihilatingZero
+    ; rawSemiring; semiring
+    ; rawRing; ring; rawField
+    )
+
+  commutativeRing : CommutativeRing _ _
+  commutativeRing = record { isCommutativeRing = isCommutativeRing }
+
+  open CommutativeRing commutativeRing public
+    using
+    ( *-commutativeMagma; *-commutativeSemigroup; *-commutativeMonoid
+    ; commutativeSemiringWithoutOne; commutativeSemiring
+    )
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 ⁻¹             ∎
diff --git a/src/Helium/Algebra/Core.agda b/src/Helium/Algebra/Core.agda
new file mode 100644
index 0000000..afe7053
--- /dev/null
+++ b/src/Helium/Algebra/Core.agda
@@ -0,0 +1,19 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- More core algebraic definitions
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+module Helium.Algebra.Core where
+
+open import Level using (_⊔_)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Nullary using (¬_)
+
+AlmostOp₁ : ∀ {a ℓ} {A : Set a} → Rel A ℓ → A → Set (a ⊔ ℓ)
+AlmostOp₁ {A = A} _≈_ ε = ∀ {x} → ¬ x ≈ ε → A
+
+AlmostOp₂ : ∀ {a ℓ} {A : Set a} → Rel A ℓ → A → Set (a ⊔ ℓ)
+AlmostOp₂ {A = A} _≈_ ε = ∀ (x : A) {y} → ¬ y ≈ ε → A
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 ⁻¹ ∙
diff --git a/src/Helium/Algebra/Structures.agda b/src/Helium/Algebra/Structures.agda
new file mode 100644
index 0000000..b64b4c7
--- /dev/null
+++ b/src/Helium/Algebra/Structures.agda
@@ -0,0 +1,162 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Some more algebraic structures
+-- (not packed up with sets, operations, etc.)
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+open import Relation.Binary.Core using (Rel)
+module Helium.Algebra.Structures
+  {a ℓ} {A : Set a} -- The underlying set
+  (_≈_ : Rel A ℓ)   -- The underlying equality relation
+  where
+
+open import Algebra.Core
+open import Algebra.Definitions _≈_
+open import Algebra.Structures _≈_
+open import Data.Product using (proj₁; proj₂)
+open import Helium.Algebra.Core
+open import Helium.Algebra.Definitions _≈_
+import Helium.Algebra.Consequences.Setoid as Consequences
+open import Level using (_⊔_)
+open import Relation.Nullary using (¬_)
+
+record IsAlmostGroup
+         (_∙_ : Op₂ A) (0# 1# : A) (_⁻¹ : AlmostOp₁ _≈_ 0#) : Set (a ⊔ ℓ) where
+  field
+    isMonoid : IsMonoid _∙_ 1#
+    inverse  : AlmostInverse 1# _⁻¹ _∙_
+    ⁻¹-cong  : AlmostCongruent₁ _⁻¹
+
+  open IsMonoid isMonoid public
+
+  infixl 6 _-_
+  _-_ : AlmostOp₂ _≈_ 0#
+  x - y≉0 = x ∙ (y≉0 ⁻¹)
+
+  inverseˡ : AlmostLeftInverse 1# _⁻¹ _∙_
+  inverseˡ = proj₁ inverse
+
+  inverseʳ : AlmostRightInverse 1# _⁻¹ _∙_
+  inverseʳ = proj₂ inverse
+
+  uniqueˡ-⁻¹ : ∀ x {y} (y≉0 : ¬ y ≈ 0#) → (x ∙ y) ≈ 1# → x ≈ (y≉0 ⁻¹)
+  uniqueˡ-⁻¹ = Consequences.assoc+id+invʳ⇒invˡ-unique
+                setoid ∙-cong assoc identity inverseʳ
+
+  uniqueʳ-⁻¹ : ∀ {x} (x≉0 : ¬ x ≈ 0#) y → (x ∙ y) ≈ 1# → y ≈ (x≉0 ⁻¹)
+  uniqueʳ-⁻¹ = Consequences.assoc+id+invˡ⇒invʳ-unique
+                setoid ∙-cong assoc identity inverseˡ
+
+record IsAlmostAbelianGroup
+         (∙ : Op₂ A) (0# 1# : A) (⁻¹ : AlmostOp₁ _≈_ 0#) : Set (a ⊔ ℓ) where
+  field
+    isAlmostGroup : IsAlmostGroup ∙ 0# 1# ⁻¹
+    comm          : Commutative ∙
+
+  open IsAlmostGroup isAlmostGroup
+
+  isCommutativeMonoid : IsCommutativeMonoid ∙ 1#
+  isCommutativeMonoid = record
+    { isMonoid = isMonoid
+    ; comm     = comm
+    }
+
+  open IsCommutativeMonoid isCommutativeMonoid public
+    using (isCommutativeMagma; isCommutativeSemigroup)
+
+record IsDivisionRing
+         (+ _*_ : Op₂ A) (-_ : Op₁ A) (0# 1# : A)
+         (_⁻¹ : AlmostOp₁ _≈_ 0#) : Set (a ⊔ ℓ) where
+  field
+    +-isAbelianGroup : IsAbelianGroup + 0# -_
+    *-isAlmostGroup  : IsAlmostGroup _*_ 0# 1# _⁻¹
+    distrib          : _*_ DistributesOver +
+    zero             : Zero 0# _*_
+
+  infixl 7 _/_
+  _/_ : AlmostOp₂ _≈_ 0#
+  x / y≉0 = x * (y≉0 ⁻¹)
+
+  open IsAbelianGroup +-isAbelianGroup public
+    renaming
+    ( assoc                  to +-assoc
+    ; ∙-cong                 to +-cong
+    ; ∙-congˡ                to +-congˡ
+    ; ∙-congʳ                to +-congʳ
+    ; identity               to +-identity
+    ; identityˡ              to +-identityˡ
+    ; identityʳ              to +-identityʳ
+    ; inverse                to -‿inverse
+    ; inverseˡ               to -‿inverseˡ
+    ; inverseʳ               to -‿inverseʳ
+    ; ⁻¹-cong                to -‿cong
+    ; uniqueˡ-⁻¹             to uniqueˡ‿-
+    ; uniqueʳ-⁻¹             to uniqueʳ‿-
+    ; comm                   to +-comm
+    ; isMagma                to +-isMagma
+    ; isSemigroup            to +-isSemigroup
+    ; isMonoid               to +-isMonoid
+    ; isCommutativeMagma     to +-isCommutativeMagma
+    ; isCommutativeMonoid    to +-isCommutativeMonoid
+    ; isCommutativeSemigroup to +-isCommutativeSemigroup
+    ; isGroup                to +-isGroup
+    )
+
+  open IsAlmostGroup *-isAlmostGroup public
+    using (⁻¹-cong; uniqueˡ-⁻¹; uniqueʳ-⁻¹)
+    renaming
+    ( assoc       to *-assoc
+    ; ∙-cong      to *-cong
+    ; ∙-congˡ     to *-congˡ
+    ; ∙-congʳ     to *-congʳ
+    ; identity    to *-identity
+    ; identityˡ   to *-identityˡ
+    ; identityʳ   to *-identityʳ
+    ; inverse     to ⁻¹-inverse
+    ; inverseˡ    to ⁻¹-inverseˡ
+    ; inverseʳ    to ⁻¹-inverseʳ
+    ; isMagma     to *-isMagma
+    ; isSemigroup to *-isSemigroup
+    ; isMonoid    to *-isMonoid
+    )
+
+  isRing : IsRing + _*_ -_ 0# 1#
+  isRing = record
+    { +-isAbelianGroup = +-isAbelianGroup
+    ; *-isMonoid = *-isMonoid
+    ; distrib = distrib
+    ; zero = zero
+    }
+
+  open IsRing isRing public
+    using
+    ( distribˡ ; distribʳ ; zeroˡ ; zeroʳ
+    ; isNearSemiring ; isSemiringWithoutOne ; isSemiringWithoutAnnihilatingZero
+    )
+
+record IsField
+         (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A)
+         (⁻¹ : AlmostOp₁ _≈_ 0#) : Set (a ⊔ ℓ) where
+  field
+    isDivisionRing : IsDivisionRing + * -_ 0# 1# ⁻¹
+    *-comm         : Commutative *
+
+  open IsDivisionRing isDivisionRing public
+
+  isCommutativeRing : IsCommutativeRing + * -_ 0# 1#
+  isCommutativeRing = record
+    { isRing = isRing
+    ; *-comm = *-comm
+    }
+
+  open IsCommutativeRing isCommutativeRing public
+    using
+    ( isCommutativeSemiring
+    ; isCommutativeSemiringWithoutOne
+    ; *-isCommutativeMagma
+    ; *-isCommutativeSemigroup
+    ; *-isCommutativeMonoid
+    )