From 278547ab5f3a36bbf2bbd114fc18f30187eab77c Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 5 Jun 2024 14:44:06 +0100 Subject: [PATCH] fix #2394 --- src/Function/Endo/Propositional.agda | 79 ++++++++++++++++------------ src/Function/Endo/Setoid.agda | 65 +++++++++++++---------- 2 files changed, 82 insertions(+), 62 deletions(-) diff --git a/src/Function/Endo/Propositional.agda b/src/Function/Endo/Propositional.agda index 6d2e8a2204..2305db5452 100644 --- a/src/Function/Endo/Propositional.agda +++ b/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,7 +21,7 @@ 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₂) @@ -27,9 +29,25 @@ 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 + } diff --git a/src/Function/Endo/Setoid.agda b/src/Function/Endo/Setoid.agda index cd36f2028f..ffe8273943 100644 --- a/src/Function/Endo/Setoid.agda +++ b/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 - }