From d5ce9a88d412d6fd71085bfebeb614e70540ca22 Mon Sep 17 00:00:00 2001
From: Jacques Carette <carette@mcmaster.ca>
Date: Wed, 27 Dec 2023 09:48:54 -0500
Subject: [PATCH 1/5] Bring back a convenient short-cut for infix Func

---
 CHANGELOG.md              | 3 +++
 src/Function/Bundles.agda | 9 +++++++++
 2 files changed, 12 insertions(+)

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..65638f2c9f 100644
--- a/src/Function/Bundles.agda
+++ b/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
 ------------------------------------------------------------------------

From 856fbf8d4bf38c253e74e481ce786764c59f81df Mon Sep 17 00:00:00 2001
From: Jacques Carette <carette@mcmaster.ca>
Date: Sat, 30 Dec 2023 09:49:51 -0500
Subject: [PATCH 2/5] change name as per suggestion from Matthew

---
 src/Function/Bundles.agda | 19 ++++++++++---------
 1 file changed, 10 insertions(+), 9 deletions(-)

diff --git a/src/Function/Bundles.agda b/src/Function/Bundles.agda
index 65638f2c9f..e41597f4b4 100644
--- a/src/Function/Bundles.agda
+++ b/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
 ------------------------------------------------------------------------

From debfec19a0b6ad93cadce4e88f559790b287a316 Mon Sep 17 00:00:00 2001
From: Jacques Carette <carette@mcmaster.ca>
Date: Sat, 30 Dec 2023 10:29:21 -0500
Subject: [PATCH 3/5] propagate use of shortcut to where it increases
 readability

---
 src/Data/Product/Function/Dependent/Setoid.agda  |  8 +++++---
 .../Product/Function/NonDependent/Setoid.agda    | 16 ++++++++--------
 src/Data/Sum/Function/Setoid.agda                | 12 ++++++------
 src/Function/Properties/Equivalence.agda         |  2 +-
 src/Function/Properties/Injection.agda           |  2 +-
 src/Function/Properties/Inverse.agda             |  4 ++--
 src/Function/Properties/Surjection.agda          |  2 +-
 7 files changed, 24 insertions(+), 22 deletions(-)

diff --git a/src/Data/Product/Function/Dependent/Setoid.agda b/src/Data/Product/Function/Dependent/Setoid.agda
index 22cb950626..1e29d13c7a 100644
--- a/src/Data/Product/Function/Dependent/Setoid.agda
+++ b/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′
diff --git a/src/Data/Product/Function/NonDependent/Setoid.agda b/src/Data/Product/Function/NonDependent/Setoid.agda
index 653f122bb5..4312e8d126 100644
--- a/src/Data/Product/Function/NonDependent/Setoid.agda
+++ b/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)
diff --git a/src/Data/Sum/Function/Setoid.agda b/src/Data/Sum/Function/Setoid.agda
index d0b28634fa..9954207ae4 100644
--- a/src/Data/Sum/Function/Setoid.agda
+++ b/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,13 +28,13 @@ 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
@@ -42,7 +42,7 @@ inj₂ₛ = record { to = inj₂ ; cong = inj₂ }
     (inj₂ x∼₂y) → cong g x∼₂y
   } where open Func
 
-swapₛ : Func (S ⊎ₛ T) (T ⊎ₛ S)
+swapₛ : (S ⊎ₛ T) ⟶ₛ (T ⊎ₛ S)
 swapₛ = [ inj₂ₛ , inj₁ₛ ]ₛ
 
 ------------------------------------------------------------------------
diff --git a/src/Function/Properties/Equivalence.agda b/src/Function/Properties/Equivalence.agda
index ad1264ec7c..247ff9f5c8 100644
--- a/src/Function/Properties/Equivalence.agda
+++ b/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
diff --git a/src/Function/Properties/Injection.agda b/src/Function/Properties/Injection.agda
index 0e773cf9b8..2250a28152 100644
--- a/src/Function/Properties/Injection.agda
+++ b/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
diff --git a/src/Function/Properties/Inverse.agda b/src/Function/Properties/Inverse.agda
index 5ade85d843..8697ac597e 100644
--- a/src/Function/Properties/Inverse.agda
+++ b/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
 
diff --git a/src/Function/Properties/Surjection.agda b/src/Function/Properties/Surjection.agda
index 6f0bc11e6b..91d450fe60 100644
--- a/src/Function/Properties/Surjection.agda
+++ b/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

From 7ef2f73ab707a66ca72e9122d11d6be743b0468d Mon Sep 17 00:00:00 2001
From: Jacques Carette <carette@mcmaster.ca>
Date: Sun, 31 Dec 2023 12:12:21 -0500
Subject: [PATCH 4/5] Revert "propagate use of shortcut to where it increases
 readability"

This reverts commit debfec19a0b6ad93cadce4e88f559790b287a316.
---
 src/Data/Product/Function/Dependent/Setoid.agda  |  8 +++-----
 .../Product/Function/NonDependent/Setoid.agda    | 16 ++++++++--------
 src/Data/Sum/Function/Setoid.agda                | 12 ++++++------
 src/Function/Properties/Equivalence.agda         |  2 +-
 src/Function/Properties/Injection.agda           |  2 +-
 src/Function/Properties/Inverse.agda             |  4 ++--
 src/Function/Properties/Surjection.agda          |  2 +-
 7 files changed, 22 insertions(+), 24 deletions(-)

diff --git a/src/Data/Product/Function/Dependent/Setoid.agda b/src/Data/Product/Function/Dependent/Setoid.agda
index 1e29d13c7a..22cb950626 100644
--- a/src/Data/Product/Function/Dependent/Setoid.agda
+++ b/src/Data/Product/Function/Dependent/Setoid.agda
@@ -14,9 +14,7 @@ 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.Base using (_$_; _∘_)
-open import Function.Bundles
-open import Function.Definitions
+open import Function
 open import Function.Consequences.Setoid
 open import Function.Properties.Injection using (mkInjection)
 open import Function.Properties.Surjection using (mkSurjection; ↠⇒⇔)
@@ -69,8 +67,8 @@ module _ where
 
   function :
     (f : I ⟶ J) →
-    (∀ {i} → (A atₛ i) ⟶ₛ (B atₛ (to f i))) →
-    I ×ₛ A ⟶ₛ J ×ₛ B
+    (∀ {i} → Func (A atₛ i) (B atₛ (to f i))) →
+    Func (I ×ₛ A) (J ×ₛ B)
   function {I = I} {J = J} {A = A} {B = B} I⟶J A⟶B = record
     { to    = to′
     ; cong  = cong′
diff --git a/src/Data/Product/Function/NonDependent/Setoid.agda b/src/Data/Product/Function/NonDependent/Setoid.agda
index 4312e8d126..653f122bb5 100644
--- a/src/Data/Product/Function/NonDependent/Setoid.agda
+++ b/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 using (_×ₛ_)
+open import Data.Product.Relation.Binary.Pointwise.NonDependent
 open import Level using (Level)
-open import Relation.Binary using (Setoid)
-open import Function.Bundles -- much of it is used
+open import Relation.Binary
+open import Function
 
 private
   variable
@@ -24,25 +24,25 @@ private
 ------------------------------------------------------------------------
 -- Combinators for equality preserving functions
 
-proj₁ₛ : A ×ₛ B ⟶ₛ A
+proj₁ₛ : Func (A ×ₛ B) A
 proj₁ₛ = record { to = proj₁ ; cong = proj₁ }
 
-proj₂ₛ : A ×ₛ B ⟶ₛ B
+proj₂ₛ : Func (A ×ₛ B) B
 proj₂ₛ = record { to = proj₂ ; cong = proj₂ }
 
-<_,_>ₛ : A ⟶ₛ B → A ⟶ₛ C → A ⟶ₛ B ×ₛ C
+<_,_>ₛ : Func A B → Func A C → Func A (B ×ₛ C)
 < f , g >ₛ = record
   { to   = < to   f , to   g >
   ; cong = < cong f , cong g >
   } where open Func
 
-swapₛ : A ×ₛ B ⟶ₛ B ×ₛ A
+swapₛ : Func (A ×ₛ B) (B ×ₛ A)
 swapₛ = < proj₂ₛ , proj₁ₛ >ₛ
 
 ------------------------------------------------------------------------
 -- Function bundles
 
-_×-function_ : A ⟶ₛ B → C ⟶ₛ D → A ×ₛ C ⟶ₛ B ×ₛ D
+_×-function_ : Func A B → Func C D → Func (A ×ₛ C) (B ×ₛ D)
 f ×-function g = record
   { to    = Prod.map (to f) (to g)
   ; cong  = Prod.map (cong f) (cong g)
diff --git a/src/Data/Sum/Function/Setoid.agda b/src/Data/Sum/Function/Setoid.agda
index 9954207ae4..d0b28634fa 100644
--- a/src/Data/Sum/Function/Setoid.agda
+++ b/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 using (Setoid; Rel)
-open import Function.Base using (_$_; _∘_)
+open import Relation.Binary
+open import Function.Base
 open import Function.Bundles
 open import Function.Definitions
 open import Level
@@ -28,13 +28,13 @@ private
 ------------------------------------------------------------------------
 -- Combinators for equality preserving functions
 
-inj₁ₛ : S ⟶ₛ (S ⊎ₛ T)
+inj₁ₛ : Func S (S ⊎ₛ T)
 inj₁ₛ = record { to = inj₁ ; cong = inj₁ }
 
-inj₂ₛ : T ⟶ₛ (S ⊎ₛ T)
+inj₂ₛ : Func T (S ⊎ₛ T)
 inj₂ₛ = record { to = inj₂ ; cong = inj₂ }
 
-[_,_]ₛ : S ⟶ₛ U → T ⟶ₛ U → S ⊎ₛ T ⟶ₛ U
+[_,_]ₛ : Func S U → Func T U → Func (S ⊎ₛ T) U
 [ f , g ]ₛ = record
   { to   = [ to f , to g ]
   ; cong = λ where
@@ -42,7 +42,7 @@ inj₂ₛ = record { to = inj₂ ; cong = inj₂ }
     (inj₂ x∼₂y) → cong g x∼₂y
   } where open Func
 
-swapₛ : (S ⊎ₛ T) ⟶ₛ (T ⊎ₛ S)
+swapₛ : Func (S ⊎ₛ T) (T ⊎ₛ S)
 swapₛ = [ inj₂ₛ , inj₁ₛ ]ₛ
 
 ------------------------------------------------------------------------
diff --git a/src/Function/Properties/Equivalence.agda b/src/Function/Properties/Equivalence.agda
index 247ff9f5c8..ad1264ec7c 100644
--- a/src/Function/Properties/Equivalence.agda
+++ b/src/Function/Properties/Equivalence.agda
@@ -29,7 +29,7 @@ private
 ------------------------------------------------------------------------
 -- Constructors
 
-mkEquivalence : S ⟶ₛ T → T ⟶ₛ S → Equivalence S T
+mkEquivalence : Func S T → Func T S → Equivalence S T
 mkEquivalence f g = record
   { to = to f
   ; from = to g
diff --git a/src/Function/Properties/Injection.agda b/src/Function/Properties/Injection.agda
index 2250a28152..0e773cf9b8 100644
--- a/src/Function/Properties/Injection.agda
+++ b/src/Function/Properties/Injection.agda
@@ -29,7 +29,7 @@ private
 ------------------------------------------------------------------------
 -- Constructors
 
-mkInjection : (f : S ⟶ₛ T) (open Func f) →
+mkInjection : (f : Func S T) (open Func f) →
               Injective Eq₁._≈_ Eq₂._≈_ to  →
               Injection S T
 mkInjection f injective = record
diff --git a/src/Function/Properties/Inverse.agda b/src/Function/Properties/Inverse.agda
index 8697ac597e..5ade85d843 100644
--- a/src/Function/Properties/Inverse.agda
+++ b/src/Function/Properties/Inverse.agda
@@ -68,11 +68,11 @@ isEquivalence = record
 ------------------------------------------------------------------------
 -- Conversion functions
 
-toFunction : Inverse S T → S ⟶ₛ T
+toFunction : Inverse S T → Func S T
 toFunction I = record { to = to ; cong = to-cong }
   where open Inverse I
 
-fromFunction : Inverse S T → T ⟶ₛ S
+fromFunction : Inverse S T → Func T S
 fromFunction I = record { to = from ; cong = from-cong }
   where open Inverse I
 
diff --git a/src/Function/Properties/Surjection.agda b/src/Function/Properties/Surjection.agda
index 91d450fe60..6f0bc11e6b 100644
--- a/src/Function/Properties/Surjection.agda
+++ b/src/Function/Properties/Surjection.agda
@@ -29,7 +29,7 @@ private
 ------------------------------------------------------------------------
 -- Constructors
 
-mkSurjection : (f : S ⟶ₛ T) (open Func f) →
+mkSurjection : (f : Func S T) (open Func f) →
               Surjective Eq₁._≈_ Eq₂._≈_ to  →
               Surjection S T
 mkSurjection f surjective = record

From 15347a445b8a8e7e93282b0c9aa02abe8b215e9c Mon Sep 17 00:00:00 2001
From: Jacques Carette <carette@mcmaster.ca>
Date: Sun, 31 Dec 2023 12:16:24 -0500
Subject: [PATCH 5/5] Move definitions up. Fix comments.

---
 src/Function/Bundles.agda | 21 +++++++++++----------
 1 file changed, 11 insertions(+), 10 deletions(-)

diff --git a/src/Function/Bundles.agda b/src/Function/Bundles.agda
index e41597f4b4..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
 ------------------------------------------------------------------------
@@ -526,16 +537,6 @@ 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
 ------------------------------------------------------------------------