change name as per suggestion from Matthew

Author: JacquesCarette

src/Function/Bundles.agda

@@ -400,15 +400,6 @@ 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
 ------------------------------------------------------------------------
@@ -535,6 +526,16 @@ module _ {A : Set a} {B : Set b} where
     , strictlyInverseʳ⇒inverseʳ to invʳ
     )
 
+------------------------------------------------------------------------
+-- Inline bbreviations for oft-used items
+--  (but one define the ones that recur)
+------------------------------------------------------------------------
+
+-- Same convention as above, with appended ₛ (for 'S'etoid)
+infixr 0 _⟶ₛ_
+_⟶ₛ_ : Setoid a ℓ₁ → Setoid b ℓ₂ → Set _
+_⟶ₛ_ = Func
+
 ------------------------------------------------------------------------
 -- Other
 ------------------------------------------------------------------------