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,17 @@ 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 _
+ 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,121 @@
+------------------------------------------------------------------------
+-- 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
+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)
+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; _∘′_; _∋_; 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
+
+fromSetoidEndo : Setoid.Endo → Endo
+fromSetoidEndo = _⟨$⟩_
+
+toSetoidEndo : Endo → Setoid.Endo
+toSetoidEndo f = record
+ { to = f
+ ; cong = cong f
+ }
+
+------------------------------------------------------------------------
+-- Structures
+
+∘-isMagma : IsMagma _≡_ _∘_
+∘-isMagma = record
+ { isEquivalence = ≡.isEquivalence
+ ; ∙-cong = cong₂ _∘_
+ }
+
+∘-magma : Magma _ _
+∘-magma = record { isMagma = ∘-isMagma }
+
+∘-isSemigroup : IsSemigroup _≡_ _∘_
+∘-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 }
+
+------------------------------------------------------------------------
+-- n-th iterated composition
+
+infixr 8 _^_
+
+_^_ : Endo → ℕ → Endo
+_^_ = flip _×_ where open RawMonoidDefinitions ∘-id-rawMonoid
+
+------------------------------------------------------------------------
+-- Homomorphism
+
+module _ (f : Endo) where
+
+ 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

@@ -0,0 +1,117 @@
+------------------------------------------------------------------------
+-- 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)
+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)
+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 raw bundles
+
+Endo : Set _
+Endo = S ⟶ₛ S
+
+private
+ id : Endo
+ id = identity S
+
+ ∘-id-rawMonoid : RawMonoid (c ⊔ e) (c ⊔ e)
+ ∘-id-rawMonoid = record { Carrier = Endo; _≈_ = _≈_ ; _∙_ = _∘_ ; ε = id }
+
+ open RawMonoid ∘-id-rawMonoid
+ using ()
+ renaming (rawMagma to ∘-rawMagma)
+
+--------------------------------------------------------------
+-- 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 }
+
+------------------------------------------------------------------------
+-- -- n-th iterated composition
+
+infixr 8 _^_
+
+_^_ : Endo → ℕ → Endo
+f ^ n = n × f where open RawMonoidDefinitions ∘-id-rawMonoid
+
+------------------------------------------------------------------------
+-- Homomorphism
+
+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
+ }
+

src/Function/Endomorphism/Propositional.agda

@@ -1,16 +1,18 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Endomorphisms on a Set
+-- This module is DEPRECATED.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
--- Disabled to prevent warnings from deprecated names
-{-# OPTIONS --warn=noUserWarning #-}
-
 module Function.Endomorphism.Propositional {a} (A : Set a) where
 
+{-# WARNING_ON_IMPORT
+"Function.Endomorphism.Propositional was deprecated in v2.1.
+Use Function.Endo.Propositional instead."
+#-}
+
 open import Algebra
 open import Algebra.Morphism; open Definitions
 

src/Function/Endomorphism/Setoid.agda

@@ -1,19 +1,21 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Endomorphisms on a Setoid
+-- This module is DEPRECATED.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
--- Disabled to prevent warnings from deprecated names
-{-# OPTIONS --warn=noUserWarning #-}
-
 open import Relation.Binary.Core using (_Preserves_⟶_)
 open import Relation.Binary.Bundles using (Setoid)
 
 module Function.Endomorphism.Setoid {c e} (S : Setoid c e) where
 
+{-# WARNING_ON_IMPORT
+"Function.Endomorphism.Setoid was deprecated in v2.1.
+Use Function.Endo.Setoid instead."
+#-}
+
 open import Agda.Builtin.Equality
 
 open import Algebra

src/Function/Equality.agda

@@ -5,7 +5,6 @@
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
-{-# OPTIONS --warn=noUserWarning #-}
 
 module Function.Equality where