Add bundled homomorphisms (#2383)

* Bundle `Algebra.Morphism`s

* more bundles!

* `RingWithoutOne` now exports a `RawRingWithoutOne` field

* disambiguation error when trying to add `RingWithoutOneHomomorphism` record

* FIXED: disambiguation error when trying to add `RingWithoutOneHomomorphism`

* add `rawKleeneAlgebra`

* add `KleeneAlgebra`, `Quasigroup`, and `Lopp` homomorphisms

* add bundled `Identity` homomorphisms

* avoid name clash: remove `open`ing of sub-homomorphism bundles

* add bundled `Composition` of homomorphisms

* more exported sub-bundles

* removed redundant anonymous `module`s

* removed redundant anonymous `module`s

* add `isNearSemiring` to `IsRingWithoutOne` plus knock-on re-exports

* add `nearSemiring` to `RingWithoutOne` plus knock-on re-exports

* add `rawNearSemiring` to `RingWithoutOne` plus knock-on re-exports

* lots more exported sub-structures and sub-bundles

* fix bug: restrict exports

* lots more exported sub-structures and sub-bundles

* refactor: `RawX` parameterisation

* knock-on: `Identity` takes a full `Bundle`

* tighten imports

* knock-on: `Composition` takes full `Bundle`s

* `CHANGELOG`

* `fix-whitespace`

* fix `CHANGELOG`

* update `CHANGELOG`

---------

Co-authored-by: MatthewDaggitt <[email protected]>

Author: jamesmckinna

CHANGELOG.md

@@ -88,6 +88,11 @@ Deprecated names
 New modules
 -----------
 
+* Bundled morphisms between (raw) algebraic structures:
+  ```
+  Algebra.Morphism.Bundles
+  ```
+
 * Properties of `IdempotentCommutativeMonoid`s refactored out from `Algebra.Solver.IdempotentCommutativeMonoid`:
   ```agda
   Algebra.Properties.IdempotentCommutativeMonoid
@@ -140,6 +145,93 @@ New modules
 Additions to existing modules
 -----------------------------
 
+* In `Algebra.Bundles.KleeneAlgebra`:
+  ```agda
+  rawKleeneAlgebra : RawKleeneAlgebra _ _
+  ```
+
+* In `Algebra.Bundles.Raw.RawRingWithoutOne`
+  ```agda
+  rawNearSemiring : RawNearSemiring c ℓ
+  ```
+
+* Exporting more `Raw` substructures from `Algebra.Bundles.Ring`:
+  ```agda
+  rawNearSemiring   : RawNearSemiring _ _
+  rawRingWithoutOne : RawRingWithoutOne _ _
+  +-rawGroup        : RawGroup _ _
+  ```
+
+* Exporting `RawRingWithoutOne` and `(Raw)NearSemiring` subbundles from
+  `Algebra.Bundles.RingWithoutOne`:
+  ```agda
+  nearSemiring      : NearSemiring _ _
+  rawNearSemiring   : RawNearSemiring _ _
+  rawRingWithoutOne : RawRingWithoutOne _ _
+  ```
+
+* In `Algebra.Morphism.Construct.Composition`:
+  ```agda
+  magmaHomomorphism          : MagmaHomomorphism M₁.rawMagma M₂.rawMagma →
+                               MagmaHomomorphism M₂.rawMagma M₃.rawMagma →
+                               MagmaHomomorphism M₁.rawMagma M₃.rawMagma
+  monoidHomomorphism         : MonoidHomomorphism M₁.rawMonoid M₂.rawMonoid →
+                               MonoidHomomorphism M₂.rawMonoid M₃.rawMonoid →
+                               MonoidHomomorphism M₁.rawMonoid M₃.rawMonoid
+  groupHomomorphism          : GroupHomomorphism M₁.rawGroup M₂.rawGroup →
+                               GroupHomomorphism M₂.rawGroup M₃.rawGroup →
+                               GroupHomomorphism M₁.rawGroup M₃.rawGroup
+  nearSemiringHomomorphism   : NearSemiringHomomorphism M₁.rawNearSemiring M₂.rawNearSemiring →
+                               NearSemiringHomomorphism M₂.rawNearSemiring M₃.rawNearSemiring →
+                               NearSemiringHomomorphism M₁.rawNearSemiring M₃.rawNearSemiring
+  semiringHomomorphism       : SemiringHomomorphism M₁.rawSemiring M₂.rawSemiring →
+                               SemiringHomomorphism M₂.rawSemiring M₃.rawSemiring →
+                               SemiringHomomorphism M₁.rawSemiring M₃.rawSemiring
+  kleeneAlgebraHomomorphism  : KleeneAlgebraHomomorphism M₁.rawKleeneAlgebra M₂.rawKleeneAlgebra →
+                               KleeneAlgebraHomomorphism M₂.rawKleeneAlgebra M₃.rawKleeneAlgebra →
+                               KleeneAlgebraHomomorphism M₁.rawKleeneAlgebra M₃.rawKleeneAlgebra
+  nearSemiringHomomorphism   : NearSemiringHomomorphism M₁.rawNearSemiring M₂.rawNearSemiring →
+                               NearSemiringHomomorphism M₂.rawNearSemiring M₃.rawNearSemiring →
+                               NearSemiringHomomorphism M₁.rawNearSemiring M₃.rawNearSemiring
+  ringWithoutOneHomomorphism : RingWithoutOneHomomorphism M₁.rawRingWithoutOne M₂.rawRingWithoutOne →
+                               RingWithoutOneHomomorphism M₂.rawRingWithoutOne M₃.rawRingWithoutOne →
+                               RingWithoutOneHomomorphism M₁.rawRingWithoutOne M₃.rawRingWithoutOne
+  ringHomomorphism           : RingHomomorphism M₁.rawRing M₂.rawRing →
+                               RingHomomorphism M₂.rawRing M₃.rawRing →
+                               RingHomomorphism M₁.rawRing M₃.rawRing
+  quasigroupHomomorphism     : QuasigroupHomomorphism M₁.rawQuasigroup M₂.rawQuasigroup →
+                               QuasigroupHomomorphism M₂.rawQuasigroup M₃.rawQuasigroup →
+                               QuasigroupHomomorphism M₁.rawQuasigroup M₃.rawQuasigroup
+  loopHomomorphism           : LoopHomomorphism M₁.rawLoop M₂.rawLoop →
+                               LoopHomomorphism M₂.rawLoop M₃.rawLoop →
+                               LoopHomomorphism M₁.rawLoop M₃.rawLoop
+  ```
+
+* In `Algebra.Morphism.Construct.Identity`:
+  ```agda
+  magmaHomomorphism          : MagmaHomomorphism M.rawMagma M.rawMagma
+  monoidHomomorphism         : MonoidHomomorphism M.rawMonoid M.rawMonoid
+  groupHomomorphism          : GroupHomomorphism M.rawGroup M.rawGroup
+  nearSemiringHomomorphism   : NearSemiringHomomorphism M.raw M.raw
+  semiringHomomorphism       : SemiringHomomorphism M.rawNearSemiring M.rawNearSemiring
+  kleeneAlgebraHomomorphism  : KleeneAlgebraHomomorphism M.rawKleeneAlgebra M.rawKleeneAlgebra
+  nearSemiringHomomorphism   : NearSemiringHomomorphism M.rawNearSemiring M.rawNearSemiring
+  ringWithoutOneHomomorphism : RingWithoutOneHomomorphism M.rawRingWithoutOne M.rawRingWithoutOne
+  ringHomomorphism           : RingHomomorphism M.rawRing M.rawRing
+  quasigroupHomomorphism     : QuasigroupHomomorphism M.rawQuasigroup M.rawQuasigroup
+  loopHomomorphism           : LoopHomomorphism M.rawLoop M.rawLoop
+  ```
+
+* In `Algebra.Morphism.Structures.RingMorphisms`
+  ```agda
+  isRingWithoutOneHomomorphism : IsRingWithoutOneHomomorphism ⟦_⟧
+  ```
+
+* In `Algebra.Morphism.Structures.RingWithoutOneMorphisms`
+  ```agda
+  isNearSemiringHomomorphism : IsNearSemiringHomomorphism ⟦_⟧
+  ```
+
 * Properties of non-divisibility in `Algebra.Properties.Magma.Divisibility`:
   ```agda
   ∤-respˡ-≈ : _∤_ Respectsˡ _≈_
@@ -157,6 +249,11 @@ Additions to existing modules
   Env = Vec Carrier
  ```
 
+* In `Algebra.Structures.RingWithoutOne`:
+  ```agda
+  isNearSemiring      : IsNearSemiring _ _
+ ```
+
 * In `Data.List.Membership.Setoid.Properties`:
   ```agda
   ∉⇒All[≉]       : x ∉ xs → All (x ≉_) xs

src/Algebra/Bundles.agda

@@ -873,6 +873,16 @@ record KleeneAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where
     ; rawSemiring; semiring
     )
 
+  rawKleeneAlgebra : RawKleeneAlgebra _ _
+  rawKleeneAlgebra = record
+    { _≈_ = _≈_
+    ; _+_ = _+_
+    ; _*_ = _*_
+    ; _⋆  = _⋆
+    ; 0#  = 0#
+    ; 1#  = 1#
+    }
+
 record Quasiring c ℓ : Set (suc (c ⊔ ℓ)) where
   infixl 7 _*_
   infixl 6 _+_
@@ -931,20 +941,33 @@ record RingWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
 
   open IsRingWithoutOne isRingWithoutOne public
 
+  nearSemiring : NearSemiring _ _
+  nearSemiring = record { isNearSemiring = isNearSemiring }
+
+  open NearSemiring nearSemiring public
+    using (*-semigroup; *-magma)
+
   +-abelianGroup : AbelianGroup _ _
   +-abelianGroup = record { isAbelianGroup = +-isAbelianGroup }
 
-  *-semigroup : Semigroup _ _
-  *-semigroup = record { isSemigroup = *-isSemigroup }
-
   open AbelianGroup +-abelianGroup public
-    using () renaming (group to +-group; invertibleMagma to +-invertibleMagma; invertibleUnitalMagma to +-invertibleUnitalMagma)
+    using ()
+    renaming (group to +-group;
+      invertibleMagma to +-invertibleMagma;
+      invertibleUnitalMagma to +-invertibleUnitalMagma)
+
+  rawRingWithoutOne : RawRingWithoutOne _ _
+  rawRingWithoutOne = record
+    { _≈_ = _≈_
+    ; _+_ = _+_
+    ; _*_ = _*_
+    ; -_  = -_
+    ; 0#  = 0#
+    }
+
+  open RawRingWithoutOne rawRingWithoutOne public
+    using (+-rawGroup; *-rawMagma; rawNearSemiring)
 
-  open Semigroup *-semigroup public
-    using () renaming
-    ( rawMagma to *-rawMagma
-    ; magma    to *-magma
-    )
 
 ------------------------------------------------------------------------
 -- Bundles with 2 binary operations, 1 unary operation & 2 elements

src/Algebra/Bundles/Raw.agda

@@ -174,6 +174,17 @@ record RawRingWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
     -_      : Op₁ Carrier
     0#      : Carrier
 
+  rawNearSemiring : RawNearSemiring c ℓ
+  rawNearSemiring = record
+    { _≈_ = _≈_
+    ; _+_ = _+_
+    ; _*_ = _*_
+    ; 0#  = 0#
+    }
+
+  open RawNearSemiring rawNearSemiring public
+    using (_≉_; *-rawMagma; +-rawMagma; +-rawMonoid)
+
   +-rawGroup : RawGroup c ℓ
   +-rawGroup = record
     { _≈_ = _≈_
@@ -182,15 +193,6 @@ record RawRingWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
     ; _⁻¹ = -_
     }
 
-  open RawGroup +-rawGroup public
-    using (_≉_) renaming (rawMagma to +-rawMagma; rawMonoid to +-rawMonoid)
-
-  *-rawMagma : RawMagma c ℓ
-  *-rawMagma = record
-    { _≈_ = _≈_
-    ; _∙_ = _*_
-    }
-
 ------------------------------------------------------------------------
 -- Raw bundles with 2 binary operations, 1 unary operation & 2 elements
 ------------------------------------------------------------------------