add: re-export multiplicative actions

Author: jamesmckinna

src/Algebra/Morphism/Bundles.agda

@@ -163,7 +163,8 @@ record KleeneAlgebraHomomorphism
   semiringHomomorphism = record { isSemiringHomomorphism = isSemiringHomomorphism }
 
   open SemiringHomomorphism semiringHomomorphism public
-    hiding (*-isMagmaHomomorphism; *-isMonoidHomomorphism; ⟦_⟧+_; _+⟦_⟧)
+    hiding (*-isMagmaHomomorphism; *-isMonoidHomomorphism
+           ; ⟦_⟧+_; _+⟦_⟧; ⟦_⟧*_; _*⟦_⟧)
 
 ------------------------------------------------------------------------
 -- Morphisms between RingWithoutOnes

src/Algebra/Morphism/Structures.agda

@@ -267,14 +267,21 @@ module NearSemiringMorphisms (R₁ : RawNearSemiring a ℓ₁) (R₂ : RawNearSe
       *-homo : Homomorphic₂ ⟦_⟧ _*₁_ _*₂_
 
     open +.IsMonoidHomomorphism +-isMonoidHomomorphism public
-      renaming (homo to +-homo; ε-homo to 0#-homo; isMagmaHomomorphism to +-isMagmaHomomorphism; ⟦_⟧∙_ to ⟦_⟧+_; _∙⟦_⟧ to _+⟦_⟧)
+      renaming (homo to +-homo; ε-homo to 0#-homo
+               ; isMagmaHomomorphism to +-isMagmaHomomorphism
+               ; ⟦_⟧∙_ to ⟦_⟧+_; _∙⟦_⟧ to _+⟦_⟧
+               )
 
     *-isMagmaHomomorphism : *.IsMagmaHomomorphism ⟦_⟧
     *-isMagmaHomomorphism = record
       { isRelHomomorphism = isRelHomomorphism
       ; homo = *-homo
       }
 
+    open *.IsMagmaHomomorphism *-isMagmaHomomorphism public
+      using ()
+      renaming (⟦_⟧∙_ to ⟦_⟧*_; _∙⟦_⟧ to _*⟦_⟧)
+
   record IsNearSemiringMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
     field
       isNearSemiringHomomorphism : IsNearSemiringHomomorphism ⟦_⟧
@@ -435,7 +442,11 @@ module RingWithoutOneMorphisms (R₁ : RawRingWithoutOne a ℓ₁) (R₂ : RawRi
       *-homo : Homomorphic₂ ⟦_⟧ _*₁_ _*₂_
 
     open +.IsGroupHomomorphism +-isGroupHomomorphism public
-      renaming (homo to +-homo; ε-homo to 0#-homo; isMagmaHomomorphism to +-isMagmaHomomorphism; isMonoidHomomorphism to +-isMonoidHomomorphism; ⟦_⟧∙_ to ⟦_⟧+_; _∙⟦_⟧ to _+⟦_⟧)
+      renaming (homo to +-homo; ε-homo to 0#-homo
+               ; isMagmaHomomorphism to +-isMagmaHomomorphism
+               ; isMonoidHomomorphism to +-isMonoidHomomorphism
+               ; ⟦_⟧∙_ to ⟦_⟧+_; _∙⟦_⟧ to _+⟦_⟧
+               )
 
     isNearSemiringHomomorphism : +*.IsNearSemiringHomomorphism ⟦_⟧
     isNearSemiringHomomorphism = record
@@ -449,6 +460,10 @@ module RingWithoutOneMorphisms (R₁ : RawRingWithoutOne a ℓ₁) (R₂ : RawRi
       ; homo = *-homo
       }
 
+    open *.IsMagmaHomomorphism *-isMagmaHomomorphism public
+      using ()
+      renaming (⟦_⟧∙_ to ⟦_⟧*_; _∙⟦_⟧ to _*⟦_⟧)
+
   record IsRingWithoutOneMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
     field
       isRingWithoutOneHomomorphism : IsRingWithoutOneHomomorphism ⟦_⟧