diff --git a/CHANGELOG.md b/CHANGELOG.md
index 12039b4aed..99616b2df2 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -180,6 +180,11 @@ Additions to existing modules
   contradiction′ : ¬ A → A → Whatever
   ```
 
+* In `Relation.Unary`
+  ```agda
+  _⊣_ : (A → B) → Pred A ℓ → Pred B _
+  ```
+
 * In `System.Random`:
   ```agda
   randomIO : IO Bool
diff --git a/src/Relation/Unary.agda b/src/Relation/Unary.agda
index 86bb80f1bb..a36547affd 100644
--- a/src/Relation/Unary.agda
+++ b/src/Relation/Unary.agda
@@ -202,7 +202,7 @@ Decidable P = ∀ x → Dec (P x)
 -- Operations on sets
 
 infix 10 ⋃ ⋂
-infixr 9 _⊢_
+infixr 9 _⊢_ _⊣_
 infixr 8 _⇒_
 infixr 7 _∩_
 infixr 6 _∪_
@@ -266,6 +266,11 @@ P ⊥′ Q = P ∩ Q ⊆′ ∅
 _⊢_ : (A → B) → Pred B ℓ → Pred A ℓ
 f ⊢ P = λ x → P (f x)
 
+-- Pushforward.
+
+_⊣_ : (A → B) → Pred A ℓ → Pred B _
+f ⊣ P = λ b → ∃ λ a → f a ≡ b × P a
+
 ------------------------------------------------------------------------
 -- Predicate combinators