using RawMonoid multiplication

src/Function/Endo/Propositional.agda

@@ -10,6 +10,8 @@ module Function.Endo.Propositional {a} (A : Set a) where
 
 open import Algebra using (Semigroup; Magma; RawMagma; Monoid; RawMonoid)
 open import Algebra.Core
+import Algebra.Definitions.RawMonoid as RawMonoidDefinitions
+import Algebra.Properties.Monoid.Mult as MonoidMultProperties
 open import Algebra.Structures using (IsMagma; IsSemigroup; IsMonoid)
 open import Algebra.Morphism
  using (module Definitions; IsMagmaHomomorphism; IsMonoidHomomorphism)
@@ -19,17 +21,33 @@ open import Data.Nat.Base using (ℕ; zero; suc; _+_; +-rawMagma; +-0-rawMonoid)
 open import Data.Nat.Properties using (+-0-monoid; +-semigroup)
 open import Data.Product.Base using (_,_)
 
-open import Function.Base using (id; _∘′_; _∋_)
+open import Function.Base using (id; _∘′_; _∋_; flip)
 open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_)
 open import Relation.Binary.Core using (_Preserves_⟶_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; cong₂)
 import Relation.Binary.PropositionalEquality.Properties as ≡
 
 import Function.Endo.Setoid (≡.setoid A) as Setoid
 
+------------------------------------------------------------------------
+-- Basic type and raw bundles
+
 Endo : Set a
 Endo = A → A
 
+private
+
+ _∘_ : Op₂ Endo
+ _∘_ = _∘′_
+
+ ∘-id-rawMonoid : RawMonoid a a
+ ∘-id-rawMonoid = record { Carrier = Endo; _≈_ = _≡_ ; _∙_ = _∘_ ; ε = id }
+
+ open RawMonoid ∘-id-rawMonoid
+ using ()
+ renaming (rawMagma to ∘-rawMagma)
+
+
 ------------------------------------------------------------------------
 -- Conversion back and forth with the Setoid-based notion of Endomorphism
 
@@ -42,32 +60,19 @@ toSetoidEndo f = record
  ; cong = cong f
  }
 
-------------------------------------------------------------------------
--- N-th composition
-
-infixr 8 _^_
-
-_^_ : Endo → ℕ → Endo
-f ^ zero = id
-f ^ suc n = f ∘′ (f ^ n)
-
-^-homo : ∀ f → Homomorphic₂ ℕ Endo _≡_ (f ^_) _+_ _∘′_
-^-homo f zero n = refl
-^-homo f (suc m) n = cong (f ∘′_) (^-homo f m n)
-
 ------------------------------------------------------------------------
 -- Structures
 
-∘-isMagma : IsMagma _≡_ (Op₂ Endo ∋ _∘′_)
+∘-isMagma : IsMagma _≡_ _∘_
 ∘-isMagma = record
  { isEquivalence = ≡.isEquivalence
- ; ∙-cong = cong₂ _∘′_
+ ; ∙-cong = cong₂ _∘_
  }
 
 ∘-magma : Magma _ _
 ∘-magma = record { isMagma = ∘-isMagma }
 
-∘-isSemigroup : IsSemigroup _≡_ (Op₂ Endo ∋ _∘′_)
+∘-isSemigroup : IsSemigroup _≡_ _∘_
 ∘-isSemigroup = record
  { isMagma = ∘-isMagma
  ; assoc = λ _ _ _ → refl
@@ -76,7 +81,7 @@ f ^ suc n = f ∘′ (f ^ n)
 ∘-semigroup : Semigroup _ _
 ∘-semigroup = record { isSemigroup = ∘-isSemigroup }
 
-∘-id-isMonoid : IsMonoid _≡_ _∘′_ id
+∘-id-isMonoid : IsMonoid _≡_ _∘_ id
 ∘-id-isMonoid = record
  { isSemigroup = ∘-isSemigroup
  ; identity = (λ _ → refl) , (λ _ → refl)
@@ -85,24 +90,32 @@ f ^ suc n = f ∘′ (f ^ n)
 ∘-id-monoid : Monoid _ _
 ∘-id-monoid = record { isMonoid = ∘-id-isMonoid }
 
-private
- ∘-rawMagma : RawMagma a a
- ∘-rawMagma = Semigroup.rawMagma ∘-semigroup
+------------------------------------------------------------------------
+-- n-th iterated composition
 
- ∘-id-rawMonoid : RawMonoid a a
- ∘-id-rawMonoid = Monoid.rawMonoid ∘-id-monoid
+infixr 8 _^_
+
+_^_ : Endo → ℕ → Endo
+_^_ = flip _×_ where open RawMonoidDefinitions ∘-id-rawMonoid
 
 ------------------------------------------------------------------------
 -- Homomorphism
 
-^-isMagmaHomomorphism : ∀ f → IsMagmaHomomorphism +-rawMagma ∘-rawMagma (f ^_)
-^-isMagmaHomomorphism f = record
- { isRelHomomorphism = record { cong = cong (f ^_) }
- ; homo = ^-homo f
- }
+module _ (f : Endo) where
 
-^-isMonoidHomomorphism : ∀ f → IsMonoidHomomorphism +-0-rawMonoid ∘-id-rawMonoid (f ^_)
-^-isMonoidHomomorphism f = record
- { isMagmaHomomorphism = ^-isMagmaHomomorphism f
- ; ε-homo = refl
- }
+ open MonoidMultProperties ∘-id-monoid
+
+ ^-homo : Homomorphic₂ ℕ Endo _≡_ (f ^_) _+_ _∘_
+ ^-homo = ×-homo-+ f
+
+ ^-isMagmaHomomorphism : IsMagmaHomomorphism +-rawMagma ∘-rawMagma (f ^_)
+ ^-isMagmaHomomorphism = record
+ { isRelHomomorphism = record { cong = cong (f ^_) }
+ ; homo = ^-homo
+ }
+
+ ^-isMonoidHomomorphism : IsMonoidHomomorphism +-0-rawMonoid ∘-id-rawMonoid (f ^_)
+ ^-isMonoidHomomorphism = record
+ { isMagmaHomomorphism = ^-isMagmaHomomorphism
+ ; ε-homo = refl
+ }

src/Function/Endo/Setoid.agda

@@ -13,6 +13,8 @@ module Function.Endo.Setoid {c e} (S : Setoid c e) where
 open import Agda.Builtin.Equality
 
 open import Algebra using (Semigroup; Magma; RawMagma; Monoid; RawMonoid)
+import Algebra.Definitions.RawMonoid as RawMonoidDefinitions
+import Algebra.Properties.Monoid.Mult as MonoidMultProperties
 open import Algebra.Structures using (IsMagma; IsSemigroup; IsMonoid)
 open import Algebra.Morphism
  using (module Definitions; IsMagmaHomomorphism; IsMonoidHomomorphism)
@@ -34,30 +36,23 @@ private
 
 
 ------------------------------------------------------------------------
--- Basic type and functions
+-- Basic type and raw bundles
 
 Endo : Set _
 Endo = S ⟶ₛ S
 
-infixr 8 _^_
-
 private
  id : Endo
  id = identity S
 
-_^_ : Endo → ℕ → Endo
-f ^ zero = id
-f ^ suc n = f ∘ (f ^ n)
-
-^-cong₂ : ∀ f → (f ^_) Preserves _≡_ ⟶ _≈_
-^-cong₂ f {n} refl = cong (f ^ n) S.refl
+ ∘-id-rawMonoid : RawMonoid (c ⊔ e) (c ⊔ e)
+ ∘-id-rawMonoid = record { Carrier = Endo; _≈_ = _≈_ ; _∙_ = _∘_ ; ε = id }
 
-^-homo : ∀ f → Homomorphic₂ ℕ Endo _≈_ (f ^_) _+_ _∘_
-^-homo f zero n = S.refl
-^-homo f (suc m) zero = ^-cong₂ f (+-identityʳ m)
-^-homo f (suc m) (suc n) = ^-homo f m (suc n)
+ open RawMonoid ∘-id-rawMonoid
+ using ()
+ renaming (rawMagma to ∘-rawMagma)
 
-------------------------------------------------------------------------
+--------------------------------------------------------------
 -- Structures
 
 ∘-isMagma : IsMagma _≈_ _∘_
@@ -87,24 +82,36 @@ f ^ suc n = f ∘ (f ^ n)
 ∘-id-monoid : Monoid (c ⊔ e) (c ⊔ e)
 ∘-id-monoid = record { isMonoid = ∘-id-isMonoid }
 
-private
- ∘-rawMagma : RawMagma (c ⊔ e) (c ⊔ e)
- ∘-rawMagma = Semigroup.rawMagma ∘-semigroup
+------------------------------------------------------------------------
+-- -- n-th iterated composition
 
- ∘-id-rawMonoid : RawMonoid (c ⊔ e) (c ⊔ e)
- ∘-id-rawMonoid = Monoid.rawMonoid ∘-id-monoid
+infixr 8 _^_
+
+_^_ : Endo → ℕ → Endo
+f ^ n = n × f where open RawMonoidDefinitions ∘-id-rawMonoid
 
 ------------------------------------------------------------------------
 -- Homomorphism
 
-^-isMagmaHomomorphism : ∀ f → IsMagmaHomomorphism +-rawMagma ∘-rawMagma (f ^_)
-^-isMagmaHomomorphism f = record
- { isRelHomomorphism = record { cong = ^-cong₂ f }
- ; homo = ^-homo f
- }
+module _ (f : Endo) where
+
+ open MonoidMultProperties ∘-id-monoid
+
+ ^-cong₂ : (f ^_) Preserves _≡_ ⟶ _≈_
+ ^-cong₂ = ×-congˡ {f}
+
+ ^-homo : Homomorphic₂ ℕ Endo _≈_ (f ^_) _+_ _∘_
+ ^-homo = ×-homo-+ f
+
+ ^-isMagmaHomomorphism : IsMagmaHomomorphism +-rawMagma ∘-rawMagma (f ^_)
+ ^-isMagmaHomomorphism = record
+ { isRelHomomorphism = record { cong = ^-cong₂ }
+ ; homo = ^-homo
+ }
+
+ ^-isMonoidHomomorphism : IsMonoidHomomorphism +-0-rawMonoid ∘-id-rawMonoid (f ^_)
+ ^-isMonoidHomomorphism = record
+ { isMagmaHomomorphism = ^-isMagmaHomomorphism
+ ; ε-homo = S.refl
+ }
 
-^-isMonoidHomomorphism : ∀ f → IsMonoidHomomorphism +-0-rawMonoid ∘-id-rawMonoid (f ^_)
-^-isMonoidHomomorphism f = record
- { isMagmaHomomorphism = ^-isMagmaHomomorphism f
- ; ε-homo = S.refl
- }