From 69c3796a1a8cea44564579ae03eaf5ac904d27de Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 28 Jan 2025 08:55:16 +0000 Subject: [PATCH 1/4] add: new definition --- CHANGELOG.md | 5 +++++ src/Relation/Binary/Core.agda | 3 +++ 2 files changed, 8 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index f16ed00b65..7eb5cde9a5 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -85,3 +85,8 @@ Additions to existing modules quasiring : Quasiring c ℓ → Quasiring (a ⊔ c) (a ⊔ ℓ) commutativeRing : CommutativeRing c ℓ → CommutativeRing (a ⊔ c) (a ⊔ ℓ) ``` + +* In `Relation.Binary.Core`: + ```agda + _Reflects_⟶_ : (A → B) → Rel B ℓ₁ → Rel A ℓ₂ → Set _ + ``` diff --git a/src/Relation/Binary/Core.agda b/src/Relation/Binary/Core.agda index 079bf296cc..1e79566fc9 100644 --- a/src/Relation/Binary/Core.agda +++ b/src/Relation/Binary/Core.agda @@ -60,6 +60,9 @@ P =[ f ]⇒ Q = P ⇒ (Q on f) _Preserves_⟶_ : (A → B) → Rel A ℓ₁ → Rel B ℓ₂ → Set _ f Preserves P ⟶ Q = P =[ f ]⇒ Q +_Reflects_⟶_ : (A → B) → Rel B ℓ₁ → Rel A ℓ₂ → Set _ +f Reflects Q ⟶ P = (Q on f) ⇒ P + -- A binary variant of _Preserves_⟶_. _Preserves₂_⟶_⟶_ : (A → B → C) → Rel A ℓ₁ → Rel B ℓ₂ → Rel C ℓ₃ → Set _ From ed1fcf29274107840c8ed132569aafc10b3b83c8 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 28 Jan 2025 08:55:40 +0000 Subject: [PATCH 2/4] refactor: use new definition --- src/Function/Definitions.agda | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/Function/Definitions.agda b/src/Function/Definitions.agda index 225dc53998..bbc9a7442e 100644 --- a/src/Function/Definitions.agda +++ b/src/Function/Definitions.agda @@ -10,9 +10,10 @@ module Function.Definitions where -open import Data.Product.Base using (∃; _×_) +open import Data.Product.Base using (∃; _×_; proj₁) +open import Function.Base using (_∘_) open import Level using (Level) -open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Core using (Rel; _Reflects_⟶_) private variable @@ -31,7 +32,7 @@ module _ Congruent f = ∀ {x y} → x ≈₁ y → f x ≈₂ f y Injective : (A → B) → Set _ - Injective f = ∀ {x y} → f x ≈₂ f y → x ≈₁ y + Injective = _Reflects _≈₂_ ⟶ _≈₁_ Surjective : (A → B) → Set _ Surjective f = ∀ y → ∃ λ x → ∀ {z} → z ≈₁ x → f z ≈₂ y From d16b15174df2c0288aae0db7e20918edfb24f433 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 28 Jan 2025 11:21:04 +0000 Subject: [PATCH 3/4] remove spurious addition to import list --- src/Function/Definitions.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Function/Definitions.agda b/src/Function/Definitions.agda index bbc9a7442e..a3ecb0cef5 100644 --- a/src/Function/Definitions.agda +++ b/src/Function/Definitions.agda @@ -10,7 +10,7 @@ module Function.Definitions where -open import Data.Product.Base using (∃; _×_; proj₁) +open import Data.Product.Base using (∃; _×_) open import Function.Base using (_∘_) open import Level using (Level) open import Relation.Binary.Core using (Rel; _Reflects_⟶_) From 4cdc8ed196f8c22c76f6a10aac3cfc3b99326039 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 28 Jan 2025 11:24:39 +0000 Subject: [PATCH 4/4] remove spurious addition to import list --- src/Function/Definitions.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Function/Definitions.agda b/src/Function/Definitions.agda index a3ecb0cef5..05b087850c 100644 --- a/src/Function/Definitions.agda +++ b/src/Function/Definitions.agda @@ -11,7 +11,6 @@ module Function.Definitions where open import Data.Product.Base using (∃; _×_) -open import Function.Base using (_∘_) open import Level using (Level) open import Relation.Binary.Core using (Rel; _Reflects_⟶_)