From e89fa26a5d476d423dd2945fdecd7c08de40270f Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Fri, 7 Jun 2024 07:14:13 -0400 Subject: [PATCH] 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 93e9e0fdf482164c0fb7e709ef8799fbc3fa0385. * Revert "fix things as per Matthew's review - though this remains a breaking change." This reverts commit d1cae72dcb3b44d4ba3c7290f3535544be32ab1e. * Revert "fix whitespace" This reverts commit 81230ecf0c8ff634433c9d17d53c9d2e8b3c1fd2. * Revert "port over two modules" This reverts commit 6619f114346e86ead3cf62b1170ab23d31056b48. * 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 --- CHANGELOG.md | 18 ++- src/Function/Endo/Propositional.agda | 121 +++++++++++++++++++ src/Function/Endo/Setoid.agda | 117 ++++++++++++++++++ src/Function/Endomorphism/Propositional.agda | 10 +- src/Function/Endomorphism/Setoid.agda | 10 +- src/Function/Equality.agda | 1 - 6 files changed, 266 insertions(+), 11 deletions(-) create mode 100644 src/Function/Endo/Propositional.agda create mode 100644 src/Function/Endo/Setoid.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 156756ff00..7d1e9b4e6c 100644 --- a/CHANGELOG.md +++ b/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 diff --git a/src/Function/Endo/Propositional.agda b/src/Function/Endo/Propositional.agda new file mode 100644 index 0000000000..4d1bb21cbb --- /dev/null +++ b/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 + } diff --git a/src/Function/Endo/Setoid.agda b/src/Function/Endo/Setoid.agda new file mode 100644 index 0000000000..99716b35db --- /dev/null +++ b/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 + } + diff --git a/src/Function/Endomorphism/Propositional.agda b/src/Function/Endomorphism/Propositional.agda index c8dd685328..7f9d99a155 100644 --- a/src/Function/Endomorphism/Propositional.agda +++ b/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 diff --git a/src/Function/Endomorphism/Setoid.agda b/src/Function/Endomorphism/Setoid.agda index a715ef5262..5d4993ecf6 100644 --- a/src/Function/Endomorphism/Setoid.agda +++ b/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 diff --git a/src/Function/Equality.agda b/src/Function/Equality.agda index 647dca7416..4748834a83 100644 --- a/src/Function/Equality.agda +++ b/src/Function/Equality.agda @@ -5,7 +5,6 @@ ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} -{-# OPTIONS --warn=noUserWarning #-} module Function.Equality where