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/Data/Product/Function/Dependent/Setoid.agda

@@ -14,7 +14,9 @@ module Data.Product.Function.Dependent.Setoid where
 open import Data.Product.Base using (map; _,_; proj₁; proj₂)
 open import Data.Product.Relation.Binary.Pointwise.Dependent as Σ
 open import Level using (Level)
-open import Function
+open import Function.Base using (_$_; _∘_)
+open import Function.Bundles
+open import Function.Definitions
 open import Function.Consequences.Setoid
 open import Function.Properties.Injection using (mkInjection)
 open import Function.Properties.Surjection using (mkSurjection; ↠⇒⇔)
@@ -67,8 +69,8 @@ module _ where
 
   function :
     (f : I ⟶ J) →
-    (∀ {i} → Func (A atₛ i) (B atₛ (to f i))) →
-    Func (I ×ₛ A) (J ×ₛ B)
+    (∀ {i} → (A atₛ i) ⟶ₛ (B atₛ (to f i))) →
+    I ×ₛ A ⟶ₛ J ×ₛ B
   function {I = I} {J = J} {A = A} {B = B} I⟶J A⟶B = record
     { to    = to′
     ; cong  = cong′

src/Data/Product/Function/NonDependent/Setoid.agda

@@ -10,10 +10,10 @@
 module Data.Product.Function.NonDependent.Setoid where
 
 open import Data.Product.Base as Prod
-open import Data.Product.Relation.Binary.Pointwise.NonDependent
+open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
 open import Level using (Level)
-open import Relation.Binary
-open import Function
+open import Relation.Binary using (Setoid)
+open import Function.Bundles -- much of it is used
 
 private
   variable
@@ -24,25 +24,25 @@ private
 ------------------------------------------------------------------------
 -- Combinators for equality preserving functions
 
-proj₁ₛ : Func (A ×ₛ B) A
+proj₁ₛ : A ×ₛ B ⟶ₛ A
 proj₁ₛ = record { to = proj₁ ; cong = proj₁ }
 
-proj₂ₛ : Func (A ×ₛ B) B
+proj₂ₛ : A ×ₛ B ⟶ₛ B
 proj₂ₛ = record { to = proj₂ ; cong = proj₂ }
 
-<_,_>ₛ : Func A B → Func A C → Func A (B ×ₛ C)
+<_,_>ₛ : A ⟶ₛ B → A ⟶ₛ C → A ⟶ₛ B ×ₛ C
 < f , g >ₛ = record
   { to   = < to   f , to   g >
   ; cong = < cong f , cong g >
   } where open Func
 
-swapₛ : Func (A ×ₛ B) (B ×ₛ A)
+swapₛ : A ×ₛ B ⟶ₛ B ×ₛ A
 swapₛ = < proj₂ₛ , proj₁ₛ >ₛ
 
 ------------------------------------------------------------------------
 -- Function bundles
 
-_×-function_ : Func A B → Func C D → Func (A ×ₛ C) (B ×ₛ D)
+_×-function_ : A ⟶ₛ B → C ⟶ₛ D → A ×ₛ C ⟶ₛ B ×ₛ D
 f ×-function g = record
   { to    = Prod.map (to f) (to g)
   ; cong  = Prod.map (cong f) (cong g)

src/Data/Sum/Function/Setoid.agda

@@ -11,8 +11,8 @@ module Data.Sum.Function.Setoid where
 open import Data.Product.Base as Prod using (_,_)
 open import Data.Sum.Base as Sum
 open import Data.Sum.Relation.Binary.Pointwise as Pointwise
-open import Relation.Binary
-open import Function.Base
+open import Relation.Binary using (Setoid; Rel)
+open import Function.Base using (_$_; _∘_)
 open import Function.Bundles
 open import Function.Definitions
 open import Level
@@ -28,21 +28,21 @@ private
 ------------------------------------------------------------------------
 -- Combinators for equality preserving functions
 
-inj₁ₛ : Func S (S ⊎ₛ T)
+inj₁ₛ : S ⟶ₛ (S ⊎ₛ T)
 inj₁ₛ = record { to = inj₁ ; cong = inj₁ }
 
-inj₂ₛ : Func T (S ⊎ₛ T)
+inj₂ₛ : T ⟶ₛ (S ⊎ₛ T)
 inj₂ₛ = record { to = inj₂ ; cong = inj₂ }
 
-[_,_]ₛ : Func S U → Func T U → Func (S ⊎ₛ T) U
+[_,_]ₛ : S ⟶ₛ U → T ⟶ₛ U → S ⊎ₛ T ⟶ₛ U
 [ f , g ]ₛ = record
   { to   = [ to f , to g ]
   ; cong = λ where
     (inj₁ x∼₁y) → cong f x∼₁y
     (inj₂ x∼₂y) → cong g x∼₂y
   } where open Func
 
-swapₛ : Func (S ⊎ₛ T) (T ⊎ₛ S)
+swapₛ : (S ⊎ₛ T) ⟶ₛ (T ⊎ₛ S)
 swapₛ = [ inj₂ₛ , inj₁ₛ ]ₛ
 
 ------------------------------------------------------------------------

src/Function/Bundles.agda

@@ -526,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
 ------------------------------------------------------------------------

src/Function/Properties/Equivalence.agda

@@ -29,7 +29,7 @@ private
 ------------------------------------------------------------------------
 -- Constructors
 
-mkEquivalence : Func S T → Func T S → Equivalence S T
+mkEquivalence : S ⟶ₛ T → T ⟶ₛ S → Equivalence S T
 mkEquivalence f g = record
   { to = to f
   ; from = to g

src/Function/Properties/Injection.agda

@@ -29,7 +29,7 @@ private
 ------------------------------------------------------------------------
 -- Constructors
 
-mkInjection : (f : Func S T) (open Func f) →
+mkInjection : (f : S ⟶ₛ T) (open Func f) →
               Injective Eq₁._≈_ Eq₂._≈_ to  →
               Injection S T
 mkInjection f injective = record

src/Function/Properties/Inverse.agda

@@ -68,11 +68,11 @@ isEquivalence = record
 ------------------------------------------------------------------------
 -- Conversion functions
 
-toFunction : Inverse S T → Func S T
+toFunction : Inverse S T → S ⟶ₛ T
 toFunction I = record { to = to ; cong = to-cong }
   where open Inverse I
 
-fromFunction : Inverse S T → Func T S
+fromFunction : Inverse S T → T ⟶ₛ S
 fromFunction I = record { to = from ; cong = from-cong }
   where open Inverse I
 

src/Function/Properties/Surjection.agda

@@ -29,7 +29,7 @@ private
 ------------------------------------------------------------------------
 -- Constructors
 
-mkSurjection : (f : Func S T) (open Func f) →
+mkSurjection : (f : S ⟶ₛ T) (open Func f) →
               Surjective Eq₁._≈_ Eq₂._≈_ to  →
               Surjection S T
 mkSurjection f surjective = record