From 97ea67109f7bd58e4fd8579c9cbd7794710f523f Mon Sep 17 00:00:00 2001
From: MatthewDaggitt <matthewdaggitt@gmail.com>
Date: Fri, 13 Oct 2023 10:51:06 +0900
Subject: [PATCH] Add _<$>_ operator for Function bundle

---
 CHANGELOG.md              |  6 ++++++
 src/Function/Bundles.agda | 13 +++++++++++++
 2 files changed, 19 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6bfd659aa9..c6f498dffd 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -3114,6 +3114,12 @@ Additions to existing modules
   execState : State s a → s → s
   ```
 
+* Added new application operator synonym to `Function.Bundles`:
+  ```agda
+  _⟨$⟩_ : Func From To → Carrier From → Carrier To
+  _⟨$⟩_ = Func.to 
+  ```
+  
 * Added new proofs in `Function.Construct.Symmetry`:
   ```
   bijective     : Bijective ≈₁ ≈₂ f → Symmetric ≈₂ → Transitive ≈₂ → Congruent ≈₁ ≈₂ f → Bijective ≈₂ ≈₁ f⁻¹
diff --git a/src/Function/Bundles.agda b/src/Function/Bundles.agda
index 1e479cf46a..a51dc4ea84 100644
--- a/src/Function/Bundles.agda
+++ b/src/Function/Bundles.agda
@@ -66,6 +66,7 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
     open IsCongruent isCongruent public
       using (module Eq₁; module Eq₂)
 
+
   record Injection : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
     field
       to          : A → B
@@ -472,3 +473,15 @@ module _ {A : Set a} {B : Set b} where
     , strictlyInverseʳ⇒inverseʳ to invʳ
     )
 
+------------------------------------------------------------------------
+-- Other
+------------------------------------------------------------------------
+
+-- Alternative syntax for the application of functions
+
+module _ {From : Setoid a ℓ₁} {To : Setoid b ℓ₂} where
+  open Setoid
+  
+  infixl 5 _⟨$⟩_
+  _⟨$⟩_ : Func From To → Carrier From → Carrier To
+  _⟨$⟩_ = Func.to