From 8d072d64a030cea7582868e8a115d406ad841725 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 2 Feb 2025 14:46:12 +0000
Subject: [PATCH] fix: add missing entries!

---
 CHANGELOG.md | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 757919f4e8..daff8029e0 100644
--- 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