Add bundled homomorphisms

CHANGELOG.md

@@ -83,6 +83,11 @@ New modules
   Algebra.Module.Bundles.Raw
   ```
 
+* Bundled morphisms between algebraic structures:
+  ```
+  Algebra.Morphism.Bundles
+ ```
+
 * Prime factorisation of natural numbers.
   ```
   Data.Nat.Primality.Factorisation
@@ -173,18 +178,36 @@ Additions to existing modules
   record SuccessorSet c ℓ : Set (suc (c ⊔ ℓ))
   ```
 
+* In `Algebra.Bundles.KleeneAlgebra`:
+  ```agda
+  rawKleeneAlgebra : RawKleeneAlgebra _ _
+  ```
+
 * In `Algebra.Bundles.Raw`
   ```agda
   record RawSuccessorSet c ℓ : Set (suc (c ⊔ ℓ))
   ```
 
+* 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.Construct.Terminal`:
   ```agda
   rawNearSemiring : RawNearSemiring c ℓ
@@ -229,12 +252,72 @@ Additions to existing modules
   rawModule          : RawModule R c ℓ
   ```
 
+* In `Algebra.Morphism.Construct.Composition`:
+  ```
+  magmaHomomorphism          : MagmaHomomorphism M₁ M₂ →
+                               MagmaHomomorphism M₂ M₃ →
+                               MagmaHomomorphism M₁ M₃
+  monoidHomomorphism         : MonoidHomomorphism M₁ M₂ →
+                               MagmaHomomorphism M₂ M₃ →
+                               MagmaHomomorphism M₁ M₃
+  groupHomomorphism          : GroupHomomorphism M₁ M₂ →
+                               MagmaHomomorphism M₂ M₃ →
+                               MagmaHomomorphism M₁ M₃
+  nearSemiringHomomorphism   : NearSemiringHomomorphism M₁ M₂ →
+                               NearSemiringHomomorphism M₂ M₃ →
+                               NearSemiringHomomorphism M₁ M₃
+  semiringHomomorphism       : SemiringHomomorphism M₁ M₂ →
+                               SemiringHomomorphism M₂ M₃ →
+                               SemiringHomomorphism M₁ M₃
+  kleeneAlgebraHomomorphism  : KleeneAlgebraHomomorphism M₁ M₂ →
+                               KleeneAlgebraHomomorphism M₂ M₃ →
+                               KleeneAlgebraHomomorphism M₁ M₃
+  ringWithoutOneHomomorphism : RingWithoutOneHomomorphism M₁ M₂ →
+                               RingWithoutOneHomomorphism M₂ M₃ →
+                               RingWithoutOneHomomorphism M₁ M₃
+  ringHomomorphism           : RingHomomorphism M₁ M₂ →
+                               RingHomomorphism M₂ M₃ →
+                               RingHomomorphism M₁ M₃
+  quasigroupHomomorphism     : QuasigroupHomomorphism M₁ M₂ →
+                               QuasigroupHomomorphism M₂ M₃ →
+                               QuasigroupHomomorphism M₁ M₃
+  loopHomomorphism           : LoopHomomorphism M₁ M₂ →
+                               LoopHomomorphism M₂ M₃ →
+                               LoopHomomorphism M₁ M₃
+  ```
+
+* In `Algebra.Morphism.Construct.Identity`:
+  ```
+  magmaHomomorphism          : MagmaHomomorphism M M
+  monoidHomomorphism         : MonoidHomomorphism M M
+  groupHomomorphism          : GroupHomomorphism M M
+  nearSemiringHomomorphism   : NearSemiringHomomorphism M M
+  semiringHomomorphism       : SemiringHomomorphism M M
+  kleeneAlgebraHomomorphism  : KleeneAlgebraHomomorphism M M
+  nearSemiringHomomorphism   : NearSemiringHomomorphism M M
+  ringWithoutOneHomomorphism : RingWithoutOneHomomorphism M M
+  ringHomomorphism           : RingHomomorphism M M
+  quasigroupHomomorphism     : QuasigroupHomomorphism M M
+  loopHomomorphism           : LoopHomomorphism M M
+  ```
+
 * In `Algebra.Morphism.Structures`
   ```agda
   module SuccessorSetMorphisms (N₁ : RawSuccessorSet a ℓ₁) (N₂ : RawSuccessorSet b ℓ₂) where
     record IsSuccessorSetHomomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _
     record IsSuccessorSetMonomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _
     record IsSuccessorSetIsomorphism  (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _
+  ```
+
+* In `Algebra.Morphism.Structures.RingMorphisms`
+  ```agda
+  isRingWithoutOneHomomorphism : IsRingWithoutOneHomomorphism ⟦_⟧
+  ```
+
+* In `Algebra.Morphism.Structures.RingWithoutOneMorphisms`
+  ```agda
+  isNearSemiringHomomorphism : IsNearSemiringHomomorphism ⟦_⟧
+  ```
 
 * In `Algebra.Properties.AbelianGroup`:
   ```
@@ -285,6 +368,7 @@ Additions to existing modules
 * In `Algebra.Structures`
   ```agda
   record IsSuccessorSet (suc# : Op₁ A) (zero# : A) : Set _
+  ```
 
 * In `Algebra.Structures.IsGroup`:
   ```agda
@@ -296,6 +380,11 @@ Additions to existing modules
   x \\ y = (x ⁻¹) ∙ y
   ```
 
+* In `Algebra.Structures.RingWithoutOne`:
+  ```agda
+  isNearSemiring      : IsNearSemiring _ _
+  ```
+
 * In `Algebra.Structures.IsCancellativeCommutativeSemiring` add the
   extra property as an exposed definition:
   ```agda

src/Algebra/Bundles.agda

@@ -810,6 +810,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 _+_
@@ -868,20 +878,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
 ------------------------------------------------------------------------