Add bundled homomorphisms

CHANGELOG.md

@@ -244,6 +244,55 @@ 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

src/Algebra/Morphism/Bundles.agda

@@ -57,8 +57,6 @@ record MonoidHomomorphism (A : Monoid a ℓa) (B : Monoid b ℓb) : Set (a ⊔ b
   magmaHomomorphism : MagmaHomomorphism A.magma B.magma
   magmaHomomorphism = record { isMagmaHomomorphism = isMagmaHomomorphism }
 
-  open MagmaHomomorphism magmaHomomorphism public
-
 ------------------------------------------------------------------------
 -- Morphisms between Groups
 ------------------------------------------------------------------------
@@ -78,8 +76,6 @@ record GroupHomomorphism (A : Group a ℓa) (B : Group b ℓb) : Set (a ⊔ b 
   monoidHomomorphism : MonoidHomomorphism A.monoid B.monoid
   monoidHomomorphism = record { isMonoidHomomorphism = isMonoidHomomorphism }
 
-  open MonoidHomomorphism monoidHomomorphism public
-
 ------------------------------------------------------------------------
 -- Morphisms between NearSemirings
 ------------------------------------------------------------------------
@@ -99,8 +95,6 @@ record NearSemiringHomomorphism (A : NearSemiring a ℓa) (B : NearSemiring b 
   +-monoidHomomorphism : MonoidHomomorphism A.+-monoid B.+-monoid
   +-monoidHomomorphism = record { isMonoidHomomorphism = +-isMonoidHomomorphism }
 
-  open MonoidHomomorphism +-monoidHomomorphism public
-
   *-magmaHomomorphism : MagmaHomomorphism A.*-magma B.*-magma
   *-magmaHomomorphism = record { isMagmaHomomorphism = *-isMagmaHomomorphism }
 
@@ -123,8 +117,6 @@ record SemiringHomomorphism (A : Semiring a ℓa) (B : Semiring b ℓb) : Set (a
   *-monoidHomomorphism : MonoidHomomorphism A.*-monoid B.*-monoid
   *-monoidHomomorphism = record { isMonoidHomomorphism = *-isMonoidHomomorphism }
 
-  open MonoidHomomorphism *-monoidHomomorphism public
-
 ------------------------------------------------------------------------
 -- Morphisms between KleeneAlgebras
 ------------------------------------------------------------------------
@@ -164,14 +156,9 @@ record RingWithoutOneHomomorphism (A : RingWithoutOne a ℓa) (B : RingWithoutOn
   +-groupHomomorphism : GroupHomomorphism A.+-group B.+-group
   +-groupHomomorphism = record { isGroupHomomorphism = +-isGroupHomomorphism }
 
-  open GroupHomomorphism +-groupHomomorphism public
-
   *-magmaHomomorphism : MagmaHomomorphism A.*-magma B.*-magma
   *-magmaHomomorphism = record { isMagmaHomomorphism = *-isMagmaHomomorphism }
 
-  open MagmaHomomorphism *-magmaHomomorphism public
-    hiding (setoidHomomorphism)
-
 ------------------------------------------------------------------------
 -- Morphisms between Rings
 ------------------------------------------------------------------------
@@ -190,8 +177,6 @@ record RingHomomorphism (A : Ring a ℓa) (B : Ring b ℓb) : Set (a ⊔ b ⊔ 
   +-groupHomomorphism : GroupHomomorphism A.+-group B.+-group
   +-groupHomomorphism = record { isGroupHomomorphism = +-isGroupHomomorphism }
 
-  open GroupHomomorphism +-groupHomomorphism public
-
   *-monoidHomomorphism : MonoidHomomorphism A.*-monoid B.*-monoid
   *-monoidHomomorphism = record { isMonoidHomomorphism = *-isMonoidHomomorphism }
 
@@ -213,8 +198,6 @@ record QuasigroupHomomorphism (A : Quasigroup a ℓa) (B : Quasigroup b ℓb) :
   magmaHomomorphism : MagmaHomomorphism A.magma B.magma
   magmaHomomorphism = record { isMagmaHomomorphism = ∙-isMagmaHomomorphism }
 
-  open MagmaHomomorphism magmaHomomorphism public
-
 ------------------------------------------------------------------------
 -- Morphisms between Loops
 ------------------------------------------------------------------------

src/Algebra/Morphism/Construct/Composition.agda

@@ -9,6 +9,7 @@
 module Algebra.Morphism.Construct.Composition where
 
 open import Algebra.Bundles
+open import Algebra.Morphism.Bundles
 open import Algebra.Morphism.Structures
 open import Function.Base using (_∘_)
 import Function.Construct.Composition as Func
@@ -423,3 +424,168 @@ module _ {K₁ : RawKleeneAlgebra a ℓ₁}
     ; surjective                  = Func.surjective (_≈_ K₁) (_≈_ K₂) (_≈_ K₃) F.surjective G.surjective
     } where module F = IsKleeneAlgebraIsomorphism f-iso; module G = IsKleeneAlgebraIsomorphism g-iso
 
+-----------------------------------------------------------------------
+-- Bundled morphisms between algebras
+------------------------------------------------------------------------
+
+-- Magma
+
+module _ {M₁ : Magma a ℓ₁}
+         {M₂ : Magma b ℓ₂}
+         {M₃ : Magma c ℓ₃}
+         (h : MagmaHomomorphism M₁ M₂)
+         (k : MagmaHomomorphism M₂ M₃)
+         where
+
+  private
+    module H = MagmaHomomorphism h
+    module K = MagmaHomomorphism k
+
+  magmaHomomorphism : MagmaHomomorphism M₁ M₃
+  magmaHomomorphism = record
+    { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧
+    ; isMagmaHomomorphism = isMagmaHomomorphism (Magma.trans M₃) H.isMagmaHomomorphism K.isMagmaHomomorphism }
+
+-- Monoid
+
+module _ {M₁ : Monoid a ℓ₁}
+         {M₂ : Monoid b ℓ₂}
+         {M₃ : Monoid c ℓ₃}
+         (h : MonoidHomomorphism M₁ M₂)
+         (k : MonoidHomomorphism M₂ M₃)
+         where
+
+  private
+    module H = MonoidHomomorphism h
+    module K = MonoidHomomorphism k
+
+  monoidHomomorphism : MonoidHomomorphism M₁ M₃
+  monoidHomomorphism = record
+    { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧
+    ; isMonoidHomomorphism = isMonoidHomomorphism (Monoid.trans M₃) H.isMonoidHomomorphism K.isMonoidHomomorphism }
+
+-- Group
+
+module _ {M₁ : Group a ℓ₁}
+         {M₂ : Group b ℓ₂}
+         {M₃ : Group c ℓ₃}
+         (h : GroupHomomorphism M₁ M₂)
+         (k : GroupHomomorphism M₂ M₃)
+         where
+
+  private
+    module H = GroupHomomorphism h
+    module K = GroupHomomorphism k
+
+  groupHomomorphism : GroupHomomorphism M₁ M₃
+  groupHomomorphism = record
+    { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧
+    ; isGroupHomomorphism = isGroupHomomorphism (Group.trans M₃) H.isGroupHomomorphism K.isGroupHomomorphism }
+
+-- NearSemiring
+
+module _ {M₁ : NearSemiring a ℓ₁}
+         {M₂ : NearSemiring b ℓ₂}
+         {M₃ : NearSemiring c ℓ₃}
+         (h : NearSemiringHomomorphism M₁ M₂)
+         (k : NearSemiringHomomorphism M₂ M₃)
+         where
+
+  private
+    module H = NearSemiringHomomorphism h
+    module K = NearSemiringHomomorphism k
+
+  nearSemiringHomomorphism : NearSemiringHomomorphism M₁ M₃
+  nearSemiringHomomorphism = record
+    { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧
+    ; isNearSemiringHomomorphism = isNearSemiringHomomorphism (NearSemiring.trans M₃) H.isNearSemiringHomomorphism K.isNearSemiringHomomorphism }
+
+-- Semiring
+
+module _ {M₁ : Semiring a ℓ₁}
+         {M₂ : Semiring b ℓ₂}
+         {M₃ : Semiring c ℓ₃}
+         (h : SemiringHomomorphism M₁ M₂)
+         (k : SemiringHomomorphism M₂ M₃)
+         where
+
+  private
+    module H = SemiringHomomorphism h
+    module K = SemiringHomomorphism k
+
+  semiringHomomorphism : SemiringHomomorphism M₁ M₃
+  semiringHomomorphism = record
+    { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧
+    ; isSemiringHomomorphism = isSemiringHomomorphism (Semiring.trans M₃) H.isSemiringHomomorphism K.isSemiringHomomorphism }
+
+-- RingWithoutOne
+
+module _ {M₁ : RingWithoutOne a ℓ₁}
+         {M₂ : RingWithoutOne b ℓ₂}
+         {M₃ : RingWithoutOne c ℓ₃}
+         (h : RingWithoutOneHomomorphism M₁ M₂)
+         (k : RingWithoutOneHomomorphism M₂ M₃)
+         where
+
+  private
+    module H = RingWithoutOneHomomorphism h
+    module K = RingWithoutOneHomomorphism k
+
+  ringWithoutOneHomomorphism : RingWithoutOneHomomorphism M₁ M₃
+  ringWithoutOneHomomorphism = record
+    { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧
+    ; isRingWithoutOneHomomorphism = isRingWithoutOneHomomorphism (RingWithoutOne.trans M₃) H.isRingWithoutOneHomomorphism K.isRingWithoutOneHomomorphism }
+
+-- Ring
+
+module _ {M₁ : Ring a ℓ₁}
+         {M₂ : Ring b ℓ₂}
+         {M₃ : Ring c ℓ₃}
+         (h : RingHomomorphism M₁ M₂)
+         (k : RingHomomorphism M₂ M₃)
+         where
+
+  private
+    module H = RingHomomorphism h
+    module K = RingHomomorphism k
+
+  ringHomomorphism : RingHomomorphism M₁ M₃
+  ringHomomorphism = record
+    { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧
+    ; isRingHomomorphism = isRingHomomorphism (Ring.trans M₃) H.isRingHomomorphism K.isRingHomomorphism }
+
+-- Quasigroup
+
+module _ {M₁ : Quasigroup a ℓ₁}
+         {M₂ : Quasigroup b ℓ₂}
+         {M₃ : Quasigroup c ℓ₃}
+         (h : QuasigroupHomomorphism M₁ M₂)
+         (k : QuasigroupHomomorphism M₂ M₃)
+         where
+
+  private
+    module H = QuasigroupHomomorphism h
+    module K = QuasigroupHomomorphism k
+
+  quasigroupHomomorphism : QuasigroupHomomorphism M₁ M₃
+  quasigroupHomomorphism = record
+    { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧
+    ; isQuasigroupHomomorphism = isQuasigroupHomomorphism (Quasigroup.trans M₃) H.isQuasigroupHomomorphism K.isQuasigroupHomomorphism }
+
+-- Loop
+
+module _ {M₁ : Loop a ℓ₁}
+         {M₂ : Loop b ℓ₂}
+         {M₃ : Loop c ℓ₃}
+         (h : LoopHomomorphism M₁ M₂)
+         (k : LoopHomomorphism M₂ M₃)
+         where
+
+  private
+    module H = LoopHomomorphism h
+    module K = LoopHomomorphism k
+
+  loopHomomorphism : LoopHomomorphism M₁ M₃
+  loopHomomorphism = record
+    { ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧
+    ; isLoopHomomorphism = isLoopHomomorphism (Loop.trans M₃) H.isLoopHomomorphism K.isLoopHomomorphism }