fix: add missing entries!

agda · Feb 2, 2025 · 8d072d6 · 8d072d6
1 parent 3c577cf
commit 8d072d6
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -152,6 +152,12 @@ Additions to existing modules
   module Section (surj :  Surjective ≈₁ ≈₂ f)
   ```
 
+* In `Function.Construct.Symmetry`:
+  ```agda
+  isBijectionWithoutCongruence : (IsBijection ≈₁ ≈₂ f) → IsBijection ≈₂ ≈₁ section
+  bijectionWithoutCongruence   : (Bijection R S) → IsBijection S R
+  ```
+
 * In `Function.Properties.Bijection`:
   ```agda
   sym : Bijection S T → Bijection T S