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