diff --git a/CHANGELOG.md b/CHANGELOG.md
index 8a3ccbdae8..a9749a79b6 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -85,3 +85,6 @@ Additions to existing modules
   ```agda
   map : (Char → Char) → String → String
   ```
+
+* In `Function.Bundles`, added `_➙_` as a synonym for `Func` that can
+  be used infix.
diff --git a/src/Function/Bundles.agda b/src/Function/Bundles.agda
index 98aac7a48c..6532715a21 100644
--- a/src/Function/Bundles.agda
+++ b/src/Function/Bundles.agda
@@ -400,6 +400,17 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
   module SplitSurjection (splitSurjection : SplitSurjection) =
     LeftInverse splitSurjection
 
+------------------------------------------------------------------------
+-- Infix abbreviations for oft-used items
+------------------------------------------------------------------------
+
+-- Same naming convention as used for propositional equality below, with
+-- appended ₛ (for 'S'etoid).
+
+infixr 0 _⟶ₛ_
+_⟶ₛ_ : Setoid a ℓ₁ → Setoid b ℓ₂ → Set _
+_⟶ₛ_ = Func
+
 ------------------------------------------------------------------------
 -- Bundles specialised for propositional equality
 ------------------------------------------------------------------------