Port two Endomorphism submodules over to new Function hierarchy

CHANGELOG.md

@@ -36,6 +36,13 @@ Deprecated modules
 * `Data.List.Relation.Binary.Sublist.Propositional.Disjoint` deprecated in favour of
   `Data.List.Relation.Binary.Sublist.Propositional.Slice`.
 
+Un-deprecated modules
+---------------------
+
+* The modules `Function.Endomorphism.Propositional` and
+  `Function.Endomorphism.Setoid` previously used the old `Function`
+  hierarchy but have now been ported to using the new one.
+
 Deprecated names
 ----------------
 
@@ -173,7 +180,14 @@ Additions to existing modules
   rawModule          : RawModule R c ℓ
   ```
 
-* In `Algebra.Properties.Group`:
+* In `Algebra.Morphism.Structures`:
+  ```agda
+  IsSemigroupHomomorphism : (A → B) → Set _
+  IsSemigroupMonomorphism : (A → B) → Set _
+  IsSemigroupIsomorphism : (A → B) → Set _
+  ```
+
+ * In `Algebra.Properties.Group`:
   ```agda
   isQuasigroup    : IsQuasigroup _∙_ _\\_ _//_
   quasigroup      : Quasigroup _ _

src/Algebra/Morphism/Structures.agda

@@ -68,6 +68,14 @@ module MagmaMorphisms (M₁ : RawMagma a ℓ₁) (M₂ : RawMagma b ℓ₂) wher
       ; surjective     = surjective
       }
 
+  IsSemigroupHomomorphism : (⟦_⟧ : A → B) → Set (a ⊔ ℓ₁ ⊔ ℓ₂)
+  IsSemigroupHomomorphism = IsMagmaHomomorphism
+
+  IsSemigroupMonomorphism : (⟦_⟧ : A → B) → Set (a ⊔ ℓ₁ ⊔ ℓ₂)
+  IsSemigroupMonomorphism = IsMagmaMonomorphism
+
+  IsSemigroupIsomorphism : (⟦_⟧ : A → B) → Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂)
+  IsSemigroupIsomorphism = IsMagmaIsomorphism
 
 ------------------------------------------------------------------------
 -- Morphisms over monoid-like structures

src/Function/Endomorphism/Propositional.agda

@@ -5,21 +5,19 @@
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
-
--- Disabled to prevent warnings from deprecated names
-{-# OPTIONS --warn=noUserWarning #-}
-
 module Function.Endomorphism.Propositional {a} (A : Set a) where
 
 open import Algebra
-open import Algebra.Morphism; open Definitions
+open import Algebra.Structures
+open import Algebra.Morphism
+open Definitions
 
-open import Data.Nat.Base using (ℕ; zero; suc; _+_)
+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.Equality using (_⟨$⟩_)
+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 ≡
@@ -37,7 +35,7 @@ fromSetoidEndo = _⟨$⟩_
 
 toSetoidEndo : Endo → Setoid.Endo
 toSetoidEndo f = record
-  { _⟨$⟩_ = f
+  { to = f
   ; cong  = cong f
   }
 
@@ -84,17 +82,24 @@ f ^ suc n = f ∘′ (f ^ n)
 ∘-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
 
-^-isSemigroupMorphism : ∀ f → IsSemigroupMorphism +-semigroup ∘-semigroup (f ^_)
+^-isSemigroupMorphism : ∀ f → IsSemigroupHomomorphism +-rawMagma ∘-rawMagma (f ^_)
 ^-isSemigroupMorphism f = record
-  { ⟦⟧-cong = cong (f ^_)
-  ; ∙-homo  = ^-homo f
+  { isRelHomomorphism = record { cong = cong (f ^_) }
+  ; homo = ^-homo f
   }
 
-^-isMonoidMorphism : ∀ f → IsMonoidMorphism +-0-monoid ∘-id-monoid (f ^_)
+^-isMonoidMorphism : ∀ f → IsMonoidHomomorphism +-0-rawMonoid ∘-id-rawMonoid (f ^_)
 ^-isMonoidMorphism f = record
-  { sm-homo = ^-isSemigroupMorphism f
-  ; ε-homo  = refl
+  { isMagmaHomomorphism = ^-isSemigroupMorphism f
+  ; ε-homo = refl
   }

src/Function/Endomorphism/Setoid.agda

@@ -6,90 +6,110 @@
 
 {-# 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
 
 open import Agda.Builtin.Equality
 
-open import Algebra
-open import Algebra.Structures
-open import Algebra.Morphism; open Definitions
-open import Function.Equality using (setoid; _⟶_; id; _∘_; cong)
-open import Data.Nat.Base using (ℕ; _+_); open ℕ
-open import Data.Nat.Properties
+open import Algebra using (Semigroup; Magma; RawMagma; Monoid; RawMonoid)
+open import Algebra.Structures using (IsMagma; IsSemigroup; IsMonoid)
+open import Algebra.Morphism
+  using (module Definitions; IsSemigroupHomomorphism; IsMonoidHomomorphism)
+open Definitions using (Homomorphic₂)
+open import Data.Nat.Base using (ℕ; _+_; +-rawMagma; +-0-rawMonoid)
+open ℕ
+open import Data.Nat.Properties using (+-semigroup; +-identityʳ)
 open import Data.Product.Base using (_,_)
-
-import Relation.Binary.Indexed.Heterogeneous.Construct.Trivial as Trivial
+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
-  module E = Setoid (setoid S (Trivial.indexedSetoid S))
+  module E = Setoid (S ⇨ S)
   open E hiding (refl)
-
+  open Func using (cong)
 ------------------------------------------------------------------------
 -- Basic type and functions
 
 Endo : Set _
-Endo = S ⟶ S
+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)
+^-cong₂ f {n} refl = cong (f ^ n) (Setoid.refl S)
 
 ^-homo : ∀ f → Homomorphic₂ ℕ Endo _≈_ (f ^_) _+_ _∘_
-^-homo f zero    n x≈y = cong (f ^ n) x≈y
-^-homo f (suc m) n x≈y = cong f (^-homo f m n x≈y)
+^-homo f zero    n           = Setoid.refl S
+^-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        = λ g f x → g (f x)
+  ; ∙-cong        = λ {_} {_} {_} {v} x≈y u≈v → S.trans u≈v (cong v x≈y)
   }
+  where
+    module S = Setoid S
 
-∘-magma : Magma _ _
+∘-magma : Magma (c ⊔ e) (c ⊔ e)
 ∘-magma = record { isMagma = ∘-isMagma }
 
 ∘-isSemigroup : IsSemigroup _≈_ _∘_
 ∘-isSemigroup = record
   { isMagma = ∘-isMagma
-  ; assoc   = λ h g f x≈y → cong h (cong g (cong f x≈y))
+  ; assoc   = λ h g f {s} → Setoid.refl S
   }
 
-∘-semigroup : Semigroup _ _
+∘-semigroup : Semigroup (c ⊔ e) (c ⊔ e)
 ∘-semigroup = record { isSemigroup = ∘-isSemigroup }
 
 ∘-id-isMonoid : IsMonoid _≈_ _∘_ id
 ∘-id-isMonoid = record
   { isSemigroup = ∘-isSemigroup
-  ; identity    = cong , cong
+  ; identity    = (λ f → Setoid.refl S) , (λ _ → Setoid.refl S)
   }
 
-∘-id-monoid : Monoid _ _
+∘-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
 
-^-isSemigroupMorphism : ∀ f → IsSemigroupMorphism +-semigroup ∘-semigroup (f ^_)
-^-isSemigroupMorphism f = record
-  { ⟦⟧-cong = ^-cong₂ f
-  ; ∙-homo  = ^-homo f
+^-isSemigroupHomomorphism : ∀ f → IsSemigroupHomomorphism +-rawMagma ∘-rawMagma (f ^_)
+^-isSemigroupHomomorphism f = record
+  { isRelHomomorphism = record { cong = ^-cong₂ f }
+  ; homo = ^-homo f
   }
 
-^-isMonoidMorphism : ∀ f → IsMonoidMorphism +-0-monoid ∘-id-monoid (f ^_)
-^-isMonoidMorphism f = record
-  { sm-homo = ^-isSemigroupMorphism f
-  ; ε-homo  = λ x≈y → x≈y
+^-isMonoidHomoorphism : ∀ f → IsMonoidHomomorphism +-0-rawMonoid ∘-id-rawMonoid (f ^_)
+^-isMonoidHomoorphism f = record
+  { isMagmaHomomorphism = record
+    { isRelHomomorphism = record { cong = ^-cong₂ f }
+    ; homo = ^-homo f
+    }
+  ; ε-homo = Setoid.refl S
   }
+