From 7ef3206f888a4ae9fe0c08f7c48e537c778cfea7 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 29 Jan 2025 10:52:58 +0000
Subject: [PATCH] add: `injection : Injection From To` to `IsRightInverse`

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

diff --git a/src/Function/Bundles.agda b/src/Function/Bundles.agda
index 54405f8155..87b4c53143 100644
--- a/src/Function/Bundles.agda
+++ b/src/Function/Bundles.agda
@@ -273,7 +273,9 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
       }
 
     open IsRightInverse isRightInverse public
-      using (module Eq₁; module Eq₂; strictlyInverseʳ)
+      using (module Eq₁; module Eq₂; strictlyInverseʳ; isInjection)
+
+    open IsInjection isInjection public using (injective)
 
     equivalence : Equivalence
     equivalence = record
@@ -281,6 +283,13 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
       ; from-cong = from-cong
       }
 
+    injection : Injection From To
+    injection = record
+      { to = to
+      ; cong = to-cong
+      ; injective = injective
+      }
+
 
   record Inverse : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
     field