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/Function/Definitions.agda b/src/Function/Definitions.agda
index 225dc53998..05b087850c 100644
--- a/src/Function/Definitions.agda
+++ b/src/Function/Definitions.agda
@@ -12,7 +12,7 @@ module Function.Definitions where
 
 open import Data.Product.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 +31,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
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 _