From 22889c75cb74e605e98e98db35e95164ecbd5f66 Mon Sep 17 00:00:00 2001
From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Date: Mon, 30 Sep 2024 18:24:03 +0100
Subject: [PATCH] Update CHANGELOG.md

Name change inherited from source update
---
 CHANGELOG.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 45e612b514..599dc03646 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -314,7 +314,7 @@ Additions to existing modules
 
 * In `Data.Product.Function.Dependent.Propositional`:
   ```agda
-  cong′ : ∀ {k} → (∀ {x} → A x ∼[ k ] B x) → Σ I A ∼[ k ] Σ I B
+  congˡ : ∀ {k} → (∀ {x} → A x ∼[ k ] B x) → Σ I A ∼[ k ] Σ I B
   ```
 
 * New lemma in `Data.Vec.Properties`: