add: injection : Injection From To to IsRightInverse

agda · Jan 29, 2025 · 7ef3206 · 7ef3206
1 parent 8ffbebf
commit 7ef3206
Showing 1 changed file with 10 additions and 1 deletion.
diff --git a/src/Function/Bundles.agda b/src/Function/Bundles.agda
@@ -273,14 +273,23 @@ 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
       { to-cong   = to-cong
       ; from-cong = from-cong
       }
 
+    injection : Injection From To
+    injection = record
+      { to = to
+      ; cong = to-cong
+      ; injective = injective
+      }
+
 
   record Inverse : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
     field