Port two Endomorphism submodules over to new Function hierarchy

CHANGELOG.md

@@ -46,6 +46,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
 ----------------
 

src/Algebra/Morphism/Structures.agda

@@ -116,7 +116,6 @@ module MagmaMorphisms (M₁ : RawMagma a ℓ₁) (M₂ : RawMagma b ℓ₂) wher
  ; surjective = surjective
  }
 
-
 ------------------------------------------------------------------------
 -- Morphisms over monoid-like structures
 ------------------------------------------------------------------------

src/Function/Endomorphism/Propositional.agda

@@ -5,21 +5,21 @@
 ------------------------------------------------------------------------
 
 {-# 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 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; _+_)
+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 +37,7 @@ fromSetoidEndo = _⟨$⟩_
 
 toSetoidEndo : Endo → Setoid.Endo
 toSetoidEndo f = record
- { _⟨$⟩_ = f
+ { to = f
  ; cong = cong f
  }
 
@@ -84,17 +84,41 @@ 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 = record
- { ⟦⟧-cong = cong (f ^_)
- ; ∙-homo  = ^-homo f
+^-isMagmaHomomorphism : ∀ f → IsMagmaHomomorphism +-rawMagma ∘-rawMagma (f ^_)
+^-isMagmaHomomorphism 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  = refl
+^-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/Endomorphism/Setoid.agda

@@ -6,90 +6,123 @@
 
 {-# 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; 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 (_,_)
-
-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))
- open E hiding (refl)
-
+ 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
+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) S.refl
 
 ^-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 = 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 = λ g f x → g (f x)
+ ; ∙-cong = λ {_} {_} {_} {v} x≈y u≈v → S.trans u≈v (cong v x≈y)
  }
 
-∘-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 = λ _ _ _ → S.refl
  }
 
-∘-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 = (λ _ → S.refl) , (λ _ → S.refl)
  }
 
-∘-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
+^-isMagmaHomomorphism : ∀ f → IsMagmaHomomorphism +-rawMagma ∘-rawMagma (f ^_)
+^-isMagmaHomomorphism 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
+^-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."
+#-}