Port two Endomorphism submodules over to new Function hierarchy (#2342)

* port over two modules

* and add to CHANGELOG

* fix whitespace

* fix warning: it was pointing to a record that did not exist.

* fix things as per Matthew's review - though this remains a breaking change.

* take care of comments from James.

* adjust CHANGELOG for what will be implemented shortly

* Revert "take care of comments from James."

This reverts commit 93e9e0f.

* Revert "fix things as per Matthew's review - though this remains a breaking change."

This reverts commit d1cae72.

* Revert "fix whitespace"

This reverts commit 81230ec.

* Revert "port over two modules"

This reverts commit 6619f11.

* rename these

* fix tiny merge issue

* get deprecations right (remove where not needed, make more global where needed)

* style guide - missing blank lines

* fix a bad merge

* fixed deprecations

* fix #2394

* minor tweaks

---------

Co-authored-by: James McKinna <[email protected]>

CHANGELOG.md

@@ -51,6 +51,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
 ----------------
 
@@ -167,6 +172,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 _ _
@@ -292,13 +302,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 using (_×_)
+
+------------------------------------------------------------------------
+-- Homomorphism
+
+module _ (f : Endo) where
+
+  open MonoidMultProperties ∘-id-monoid using (×-homo-+)
+
+  ^-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 using (_≡_)
+
+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 using (_×_)
+
+------------------------------------------------------------------------
+-- Homomorphism
+
+module _ (f : Endo) where
+
+  open MonoidMultProperties ∘-id-monoid using (×-congˡ; ×-homo-+)
+
+  ^-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