fix: add more fields/missing CHANGELOG entries!

agda · Feb 2, 2025 · 86dab2d · 86dab2d
1 parent 0997c71
commit 86dab2d
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 1 deletion.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -172,6 +172,17 @@ Additions to existing modules
   strictlyInverseʳ : StrictlyInverseʳ _≈₁_ f section
   ```
 
+* In `Function.Structures.IsLeftInverse`:
+  ```agda
+  surjective : Surjective _≈₁_ _≈₂_ to
+  ```
+
+* In `Function.Structures.IsRightInverse`:
+  ```agda
+  injective   : Injective _≈₁_ _≈₂_ to
+  isInjection : IsInjection to
+  ```
+
 * In `Function.Structures.IsSurjection`:
   ```agda
   section          : B → A

diff --git a/src/Function/Structures.agda b/src/Function/Structures.agda
@@ -115,10 +115,12 @@ record IsLeftInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁
   strictlyInverseˡ : StrictlyInverseˡ _≈₂_ to from
   strictlyInverseˡ _ = inverseˡ Eq₁.refl
 
+  surjective = inverseˡ⇒surjective Eq₁.setoid Eq₂.setoid inverseˡ
+
   isSurjection : IsSurjection to
   isSurjection = record
     { isCongruent = isCongruent
-    ; surjective = inverseˡ⇒surjective Eq₁.setoid Eq₂.setoid inverseˡ
+    ; surjective = surjective
     }