add: injective and isInjection to IsRightInverse

agda · Jan 29, 2025 · 8ffbebf · 8ffbebf
1 parent 9f86e57
commit 8ffbebf
Showing 1 changed file with 9 additions and 0 deletions.
diff --git a/src/Function/Structures.agda b/src/Function/Structures.agda
@@ -135,6 +135,15 @@ record IsRightInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁
   strictlyInverseʳ : StrictlyInverseʳ _≈₁_ to from
   strictlyInverseʳ = inverseʳ⇒strictlyInverseʳ _≈₁_ _≈₂_ Eq₂.refl inverseʳ
 
+  injective : Injective _≈₁_ _≈₂_ to
+  injective = inverseʳ⇒injective {f⁻¹ = from} _≈₂_ to Eq₂.refl Eq₁.sym Eq₁.trans inverseʳ
+
+  isInjection : IsInjection to
+  isInjection = record
+    { isCongruent = isCongruent
+    ; injective   = injective
+    }
+
 
 record IsInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
   field