From e820bd7859de8bcc4cfe8ac5922ae3ff02f6dc33 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?=
 <carlos.tome.cortinas@gmail.com>
Date: Thu, 6 Mar 2025 14:55:01 +0100
Subject: [PATCH 1/2] Add Dec for unit and empty types

---
 src/Relation/Nullary/Decidable/Core.agda | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index 3715c248e9..4c04c33704 100644
--- a/src/Relation/Nullary/Decidable/Core.agda
+++ b/src/Relation/Nullary/Decidable/Core.agda
@@ -18,7 +18,8 @@ open import Agda.Builtin.Maybe using (Maybe; just; nothing)
 open import Agda.Builtin.Equality using (_≡_)
 open import Level using (Level)
 open import Data.Bool.Base using (Bool; T; false; true; not; _∧_; _∨_)
-open import Data.Unit.Polymorphic.Base using (⊤)
+open import Data.Unit.Polymorphic.Base using (⊤; tt)
+open import Data.Empty.Polymorphic using (⊥)
 open import Data.Product.Base using (_×_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Function.Base using (_∘_; const; _$_; flip)
@@ -95,10 +96,18 @@ T? x = x because T-reflects x
 does  (¬? a?) = not (does a?)
 proof (¬? a?) = ¬-reflects (proof a?)
 
+⊤-dec : Dec {a} ⊤
+does  ⊤-dec = true
+proof ⊤-dec = ofʸ tt
+
 _×-dec_ : Dec A → Dec B → Dec (A × B)
 does  (a? ×-dec b?) = does a? ∧ does b?
 proof (a? ×-dec b?) = proof a? ×-reflects proof b?
 
+⊥-dec : Dec {a} ⊥
+does  ⊥-dec  = false
+proof ⊥-dec  = ofⁿ λ ()
+
 _⊎-dec_ : Dec A → Dec B → Dec (A ⊎ B)
 does  (a? ⊎-dec b?) = does a? ∨ does b?
 proof (a? ⊎-dec b?) = proof a? ⊎-reflects proof b?

From 30cfba070282476c123e22d6ae33acb2c6684a6e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?=
 <carlos.tome.cortinas@gmail.com>
Date: Thu, 6 Mar 2025 15:38:03 +0100
Subject: [PATCH 2/2] Add changes to CHANGELOG.md

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 225b699338..a73d6a1c70 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -149,3 +149,9 @@ Additions to existing modules
   ```agda
   filter-↭ : ∀ (P? : Pred.Decidable P) → xs ↭ ys → filter P? xs ↭ filter P? ys
   ```
+
+* In `Relation.Nullary.Decidable.Core`:
+  ```agda
+  ⊤-dec : Dec {a} ⊤
+  ⊥-dec : Dec {a} ⊥
+  ```