diff --git a/CHANGELOG.md b/CHANGELOG.md
index a1f857982a..0e5f17fd88 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -320,3 +320,9 @@ Additions to existing modules
   ```agda
   contra-diagonal : (A → ¬ A) → ¬ A
   ```
+
+* In `Relation.Nullary.Reflects`:
+  ```agda
+  ⊤-reflects : Reflects (⊤ {a}) true
+  ⊥-reflects : Reflects (⊥ {a}) false
+  ```
diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index e82e2b2b51..9a2f72bf81 100644
--- a/src/Relation/Nullary/Decidable/Core.agda
+++ b/src/Relation/Nullary/Decidable/Core.agda
@@ -17,7 +17,7 @@ open import Agda.Builtin.Equality using (_≡_)
 open import Agda.Builtin.Maybe using (Maybe; just; nothing)
 open import Level using (Level)
 open import Data.Bool.Base using (Bool; T; false; true; not; _∧_; _∨_)
-open import Data.Unit.Polymorphic.Base using (⊤; tt)
+open import Data.Unit.Polymorphic.Base using (⊤)
 open import Data.Empty.Polymorphic using (⊥)
 open import Data.Product.Base using (_×_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
@@ -99,7 +99,7 @@ proof (¬? a?) = ¬-reflects (proof a?)
 
 ⊤-dec : Dec {a} ⊤
 does  ⊤-dec = true
-proof ⊤-dec = ofʸ tt
+proof ⊤-dec = ⊤-reflects
 
 _×-dec_ : Dec A → Dec B → Dec (A × B)
 does  (a? ×-dec b?) = does a? ∧ does b?
@@ -107,7 +107,7 @@ proof (a? ×-dec b?) = proof a? ×-reflects proof b?
 
 ⊥-dec : Dec {a} ⊥
 does  ⊥-dec  = false
-proof ⊥-dec  = ofⁿ λ ()
+proof ⊥-dec  = ⊥-reflects
 
 _⊎-dec_ : Dec A → Dec B → Dec (A ⊎ B)
 does  (a? ⊎-dec b?) = does a? ∨ does b?
diff --git a/src/Relation/Nullary/Reflects.agda b/src/Relation/Nullary/Reflects.agda
index 00cee309a7..f89fbcf313 100644
--- a/src/Relation/Nullary/Reflects.agda
+++ b/src/Relation/Nullary/Reflects.agda
@@ -13,6 +13,8 @@ open import Agda.Builtin.Equality
 open import Data.Bool.Base
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
+open import Data.Unit.Polymorphic.Base using (⊤)
+open import Data.Empty.Polymorphic using (⊥)
 open import Level using (Level)
 open import Function.Base using (_$_; _∘_; const; id)
 open import Relation.Nullary.Negation.Core
@@ -66,21 +68,25 @@ recompute-constant : ∀ {b} (r : Reflects A b) (p q : A) →
 recompute-constant = Recomputable.recompute-constant ∘ recompute
 
 ------------------------------------------------------------------------
--- Interaction with negation, product, sums etc.
+-- Interaction with true, false, negation, product, sums etc.
 
 infixr 1 _⊎-reflects_
 infixr 2 _×-reflects_ _→-reflects_
 
+⊥-reflects : Reflects (⊥ {a}) false
+⊥-reflects = of λ()
+
+⊤-reflects : Reflects (⊤ {a}) true
+⊤-reflects = of _
+
 T-reflects : ∀ b → Reflects (T b) b
 T-reflects true  = of _
 T-reflects false = of id
 
--- If we can decide A, then we can decide its negation.
 ¬-reflects : ∀ {b} → Reflects A b → Reflects (¬ A) (not b)
 ¬-reflects (ofʸ  a) = of (_$ a)
 ¬-reflects (ofⁿ ¬a) = of ¬a
 
--- If we can decide A and Q then we can decide their product
 _×-reflects_ : ∀ {a b} → Reflects A a → Reflects B b →
                Reflects (A × B) (a ∧ b)
 ofʸ  a ×-reflects ofʸ  b = of (a , b)