From d72b95dafcf30cbea8602f308fd32702f9e5b60a Mon Sep 17 00:00:00 2001
From: Guilherme <guilhermehas@hotmail.com>
Date: Sun, 18 Feb 2024 14:23:03 +0100
Subject: [PATCH] added changelog information

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 7fa21bf90e..78e03d6126 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -187,3 +187,8 @@ Additions to existing modules
   ```agda
   ⌊⌋-map′ : (a? : Dec A) → ⌊ map′ t f a? ⌋ ≡ ⌊ a? ⌋
   ```
+
+* Added new definition in `Data.Maybe.Relation.Unary.AllBoth`:
+  ```agda
+  data AllBoth (P : Pred A p) (Q : Set q) : Pred (Maybe A) (a ⊔ p ⊔ q)
+  ```