Port two Endomorphism submodules over to new Function hierarchy

CHANGELOG.md

@@ -46,6 +46,11 @@ Deprecated modules
 * `Data.List.Relation.Binary.Sublist.Propositional.Disjoint` deprecated in favour of
   `Data.List.Relation.Binary.Sublist.Propositional.Slice`.
 
+* The modules `Function.Endomorphism.Propositional` and
+  `Function.Endomorphism.Setoid` that use the old `Function`
+  hierarchy. Use `Function.Endo.Propositional` and
+  `Function.Endo.Setoid` instead.
+
 Deprecated names
 ----------------
 
@@ -131,6 +136,11 @@ New modules
   indexedSetoid        : {A : Set a} → IndexedSetoid ℕ a _
   ```
 
+* The modules `Function.Endo.Propositional` and
+  `Function.Endo.Setoid` are new but are actually proper ports of
+  `Function.Endomorphism.Propositional` and
+  `Function.Endomorphism.Setoid`.
+
 * `Function.Relation.Binary.Equality`
   ```agda
   setoid : Setoid a₁ a₂ → Setoid b₁ b₂ → Setoid _ _
@@ -235,13 +245,12 @@ Additions to existing modules
   rawModule          : RawModule R c ℓ
   ```
 
-* In `Algebra.Morphism.Structures`
+* 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 _
-
+  IsSemigroupHomomorphism : (A → B) → Set _
+  IsSemigroupMonomorphism : (A → B) → Set _
+  IsSemigroupIsomorphism : (A → B) → Set _
+  ```
 * In `Algebra.Properties.AbelianGroup`:
   ```
   ⁻¹-anti-homo‿- : (x - y) ⁻¹ ≈ y - x

src/Function/Endo/Propositional.agda

@@ -0,0 +1,124 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Endomorphisms on a Set
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+module Function.Endo.Propositional {a} (A : Set a) where
+
+open import Algebra using (Semigroup; Magma; RawMagma; Monoid; RawMonoid)
+open import Algebra.Core
+open import Algebra.Structures using (IsMagma; IsSemigroup; IsMonoid)
+open import Algebra.Morphism
+  using (module Definitions; IsMagmaHomomorphism; IsMonoidHomomorphism)
+open Definitions using (Homomorphic₂)
+
+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.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
+
+Endo : Set a
+Endo = A → A
+
+------------------------------------------------------------------------
+-- Conversion back and forth with the Setoid-based notion of Endomorphism
+
+fromSetoidEndo : Setoid.Endo → Endo
+fromSetoidEndo = _⟨$⟩_
+
+toSetoidEndo : Endo → Setoid.Endo
+toSetoidEndo f = record
+  { to = f
+  ; 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 = record
+  { isEquivalence = ≡.isEquivalence
+  ; ∙-cong        = cong₂ _∘′_
+  }
+
+∘-magma : Magma _ _
+∘-magma = record { isMagma = ∘-isMagma }
+
+∘-isSemigroup : IsSemigroup _≡_ (Op₂ Endo ∋ _∘′_)
+∘-isSemigroup = record
+  { isMagma = ∘-isMagma
+  ; assoc   = λ _ _ _ → refl
+  }
+
+∘-semigroup : Semigroup _ _
+∘-semigroup = record { isSemigroup = ∘-isSemigroup }
+
+∘-id-isMonoid : IsMonoid _≡_ _∘′_ id
+∘-id-isMonoid = record
+  { isSemigroup = ∘-isSemigroup
+  ; identity    = (λ _ → refl) , (λ _ → refl)
+  }
+
+∘-id-monoid : Monoid _ _
+∘-id-monoid = record { isMonoid = ∘-id-isMonoid }
+
+private
+  ∘-rawMagma : RawMagma a a
+  ∘-rawMagma = Semigroup.rawMagma ∘-semigroup
+
+  ∘-id-rawMonoid : RawMonoid a a
+  ∘-id-rawMonoid = Monoid.rawMonoid ∘-id-monoid
+
+------------------------------------------------------------------------
+-- Homomorphism
+
+^-isMagmaHomomorphism : ∀ f → IsMagmaHomomorphism +-rawMagma ∘-rawMagma (f ^_)
+^-isMagmaHomomorphism f = record
+  { isRelHomomorphism = record { cong = cong (f ^_) }
+  ; homo = ^-homo f
+  }
+
+^-isMonoidHomomorphism : ∀ f → IsMonoidHomomorphism +-0-rawMonoid ∘-id-rawMonoid (f ^_)
+^-isMonoidHomomorphism f = record
+  { isMagmaHomomorphism = ^-isMagmaHomomorphism f
+  ; ε-homo = refl
+  }
+
+------------------------------------------------------------------------
+-- Deprecations
+
+-- Version 2.1
+
+^-isSemigroupMorphism = ^-isMagmaHomomorphism
+{-# WARNING_ON_USAGE ^-isSemigroupMorphism
+"Warning: ^-isSemigroupMorphism was deprecated in v2.1.
+Please use ^-isMagmaHomomorphism instead."
+#-}
+
+^-isMonoidMorphism = ^-isMonoidHomomorphism
+{-# WARNING_ON_USAGE ^-isMonoidMorphism
+"Warning: ^-isMonoidMorphism was deprecated in v2.1.
+Please use ^-isMonoidHomomorphism instead."
+#-}

src/Function/Endo/Setoid.agda

@@ -0,0 +1,128 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Endomorphisms on a Setoid
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Relation.Binary.Bundles using (Setoid)
+
+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)
+open import Algebra.Structures using (IsMagma; IsSemigroup; IsMonoid)
+open import Algebra.Morphism
+  using (module Definitions; IsMagmaHomomorphism; IsMonoidHomomorphism)
+open Definitions using (Homomorphic₂)
+open import Data.Nat.Base using (ℕ; zero; suc; _+_; +-rawMagma; +-0-rawMonoid)
+open import Data.Nat.Properties using (+-semigroup; +-identityʳ)
+open import Data.Product.Base using (_,_)
+open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_)
+open import Function.Construct.Identity using () renaming (function to identity)
+open import Function.Construct.Composition using () renaming (function to _∘_)
+open import Function.Relation.Binary.Setoid.Equality as Eq using (_⇨_)
+open import Level using (Level; _⊔_)
+open import Relation.Binary.Core using (_Preserves_⟶_)
+
+private
+  open module E = Setoid (S ⇨ S) hiding (refl)
+  module S = Setoid S
+  open Func using (cong)
+------------------------------------------------------------------------
+-- Basic type and functions
+
+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
+
+^-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)
+
+------------------------------------------------------------------------
+-- Structures
+
+∘-isMagma : IsMagma _≈_ _∘_
+∘-isMagma = record
+  { isEquivalence = isEquivalence
+  ; ∙-cong        = λ {_} {_} {_} {v} x≈y u≈v → S.trans u≈v (cong v x≈y)
+  }
+
+∘-magma : Magma (c ⊔ e) (c ⊔ e)
+∘-magma = record { isMagma = ∘-isMagma }
+
+∘-isSemigroup : IsSemigroup _≈_ _∘_
+∘-isSemigroup = record
+  { isMagma = ∘-isMagma
+  ; assoc   = λ _ _ _ → S.refl
+  }
+
+∘-semigroup : Semigroup (c ⊔ e) (c ⊔ e)
+∘-semigroup = record { isSemigroup = ∘-isSemigroup }
+
+∘-id-isMonoid : IsMonoid _≈_ _∘_ id
+∘-id-isMonoid = record
+  { isSemigroup = ∘-isSemigroup
+  ; identity    = (λ _ → S.refl) , (λ _ → S.refl)
+  }
+
+∘-id-monoid : Monoid (c ⊔ e) (c ⊔ e)
+∘-id-monoid = record { isMonoid = ∘-id-isMonoid }
+
+private
+  ∘-rawMagma : RawMagma (c ⊔ e) (c ⊔ e)
+  ∘-rawMagma = Semigroup.rawMagma ∘-semigroup
+
+  ∘-id-rawMonoid : RawMonoid (c ⊔ e) (c ⊔ e)
+  ∘-id-rawMonoid = Monoid.rawMonoid ∘-id-monoid
+
+------------------------------------------------------------------------
+-- Homomorphism
+
+^-isMagmaHomomorphism : ∀ f → IsMagmaHomomorphism +-rawMagma ∘-rawMagma (f ^_)
+^-isMagmaHomomorphism f = record
+  { isRelHomomorphism = record { cong = ^-cong₂ f }
+  ; homo = ^-homo f
+  }
+
+^-isMonoidHomomorphism : ∀ f → IsMonoidHomomorphism +-0-rawMonoid ∘-id-rawMonoid (f ^_)
+^-isMonoidHomomorphism f = record
+  { isMagmaHomomorphism = record
+    { isRelHomomorphism = record { cong = ^-cong₂ f }
+    ; homo = ^-homo f
+    }
+  ; ε-homo = S.refl
+  }
+
+------------------------------------------------------------------------
+-- Deprecations
+
+-- Version 2.1
+
+^-isSemigroupMorphism = ^-isMagmaHomomorphism
+{-# WARNING_ON_USAGE ^-isSemigroupMorphism
+"Warning: ^-isSemigroupMorphism was deprecated in v2.1.
+Please use ^-isMagmaHomomorphism instead."
+#-}
+
+^-isMonoidMorphism = ^-isMonoidHomomorphism
+{-# WARNING_ON_USAGE ^-isMonoidMorphism
+"Warning: ^-isMonoidMorphism was deprecated in v2.1.
+Please use ^-isMonoidHomomorphism instead."
+#-}