Add bundled homomorphisms

CHANGELOG.md

@@ -138,6 +138,11 @@ New modules
   Algebra.Module.Construct.Idealization
   ```
 
+* Bundled morphisms between (raw) algebraic structures:
+  ```
+  Algebra.Morphism.Bundles
+  ```
+
 * The unique morphism from the initial, resp. terminal, algebra:
   ```agda
   Algebra.Morphism.Construct.Initial
@@ -162,13 +167,48 @@ New modules
   Data.List.Relation.Binary.Equality.Setoid.Properties
   ```
 
+* Pointwise and equality relations over indexed containers:
+  ```agda
+  Data.Container.Indexed.Relation.Binary.Pointwise
+  Data.Container.Indexed.Relation.Binary.Pointwise.Properties
+  Data.Container.Indexed.Relation.Binary.Equality.Setoid
+  ```
+
+* Refactoring of `Data.List.Base.{scanr|scanl}` and their properties:
+  ```
+  Data.List.Scans.Base
+  Data.List.Scans.Properties
+  ```
+
+* Properties of `List` modulo `Setoid` equality (currently only the ([],++) monoid):
+  ```
+  Data.List.Relation.Binary.Equality.Setoid.Properties
+  ```
+
 * `Data.List.Relation.Binary.Sublist.Propositional.Slice`
   replacing `Data.List.Relation.Binary.Sublist.Propositional.Disjoint` (*)
   and adding new functions:
   - `⊆-upper-bound-is-cospan` generalising `⊆-disjoint-union-is-cospan` from (*)
   - `⊆-upper-bound-cospan` generalising `⊆-disjoint-union-cospan` from (*)
   ```
 
+* Decidability for the subset relation on lists:
+  ```agda
+  Data.List.Relation.Binary.Subset.DecSetoid (_⊆?_)
+  Data.List.Relation.Binary.Subset.DecPropositional
+  ```
+
+* Decidability for the disjoint relation on lists:
+  ```agda
+  Data.List.Relation.Binary.Disjoint.DecSetoid (disjoint?)
+  Data.List.Relation.Binary.Disjoint.DecPropositional
+  ```
+
+* Prime factorisation of natural numbers.
+  ```
+  Data.Nat.Primality.Factorisation
+  ```
+
 * Prime factorisation of natural numbers.
   ```
   Data.Nat.Primality.Factorisation
@@ -208,13 +248,19 @@ New modules
   Induction.InfiniteDescent
   ```
 
+* New IO primitives to handle buffering
+  ```agda
+  IO.Primitive.Handle
+  IO.Handle
+  ```
+
 * Symmetric interior of a binary relation
   ```
   Relation.Binary.Construct.Interior.Symmetric
-  ```
+ ```
 
 * Properties of `Setoid`s with decidable equality relation:
-  ```
+  ```agda
   Relation.Binary.Properties.DecSetoid
   ```
 
@@ -224,12 +270,6 @@ New modules
   ```
   with `Recomputable` exported publicly from `Relation.Nullary`.
 
-* New IO primitives to handle buffering
-  ```agda
-  IO.Primitive.Handle
-  IO.Handle
-  ```
-
 * `System.Random` bindings:
   ```agda
   System.Random.Primitive
@@ -296,18 +336,36 @@ Additions to existing modules
   ```
 
 
+* 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 ℓ
@@ -352,19 +410,78 @@ Additions to existing modules
   rawModule          : RawModule R c ℓ
   ```
 
+* 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`:
   ```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 _
+    record IsSuccessorSetIsomorphism  (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _
+  ```
 
-  IsSemigroupHomomorphism : (A → B) → Set _
-  IsSemigroupMonomorphism : (A → B) → Set _
-  IsSemigroupIsomorphism : (A → B) → Set _
+* In `Algebra.Morphism.Structures.RingMorphisms`
+  ```agda
+  isRingWithoutOneHomomorphism : IsRingWithoutOneHomomorphism ⟦_⟧
   ```
-* In `Algebra.Properties.AbelianGroup`:
+
+* In `Algebra.Morphism.Structures.RingWithoutOneMorphisms`
+  ```agda
+  isNearSemiringHomomorphism : IsNearSemiringHomomorphism ⟦_⟧
   ```
+
+* In `Algebra.Properties.AbelianGroup`:
+  ```agda
   ⁻¹-anti-homo‿- : (x - y) ⁻¹ ≈ y - x
   ```
 
@@ -433,6 +550,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

@@ -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
 ------------------------------------------------------------------------