Bring back a convenient short-cut for infix Func (#2239)

* Bring back a convenient short-cut for infix Func

* change name as per suggestion from Matthew

* propagate use of shortcut to where it increases readability

* Revert "propagate use of shortcut to where it increases readability"

This reverts commit debfec1.

* Move definitions up. Fix comments.

Author: JacquesCarette

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.

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
 ------------------------------------------------------------------------