From b6ec2e62197e884c4bde3dbdcc49b573d20f6835 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 5 Sep 2024 06:45:52 +0100 Subject: [PATCH] fix `CHANGELOG` after #2418 --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index ba99cf435c..9972e8f93b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -151,7 +151,7 @@ Additions to existing modules does-≡ : (a? b? : Dec A) → does a? ≡ does b? ``` -* In `Relation.Nullary.Properties`: +* In `Relation.Unary.Properties`: ```agda map : P ≐ Q → Decidable P → Decidable Q does-≐ : P ≐ Q → (P? : Decidable P) → (Q? : Decidable Q) → does ∘ P? ≗ does ∘ Q?