Bring back a convenient short-cut for infix Func

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,15 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
   module SplitSurjection (splitSurjection : SplitSurjection) =
     LeftInverse splitSurjection
 
+------------------------------------------------------------------------
+-- Inline bbreviations for oft-used items
+------------------------------------------------------------------------
+
+-- Since ⟶ is taken below, use a thick arrow instead
+infixr 0 _➙_
+_➙_ : Setoid a ℓ₁ → Setoid b ℓ₂ → Set _
+_➙_ = Func
+
 ------------------------------------------------------------------------
 -- Bundles specialised for propositional equality
 ------------------------------------------------------------------------