diff --git a/CHANGELOG.md b/CHANGELOG.md
index 562c089ddf..1d88b1bca5 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1727,6 +1727,11 @@ Deprecated names
   invPreorder   ↦ converse-preorder
   ```
 
+* In `Relation.Unary.Consequences`:
+  ```agda
+  dec⟶recomputable  ↦  dec⇒recomputable
+  ```
+
 ## Missing fixity declarations added
 
 * An effort has been made to add sensible fixities for many declarations:
diff --git a/src/Relation/Unary/Consequences.agda b/src/Relation/Unary/Consequences.agda
index 1b23578161..75c046c375 100644
--- a/src/Relation/Unary/Consequences.agda
+++ b/src/Relation/Unary/Consequences.agda
@@ -11,5 +11,19 @@ module Relation.Unary.Consequences where
 open import Relation.Unary
 open import Relation.Nullary using (recompute)
 
-dec⟶recomputable : {a ℓ : _} {A : Set a} {P : Pred A ℓ} → Decidable P → Recomputable P
-dec⟶recomputable P-dec = recompute (P-dec _)
+dec⇒recomputable : {a ℓ : _} {A : Set a} {P : Pred A ℓ} → Decidable P → Recomputable P
+dec⇒recomputable P-dec = recompute (P-dec _)
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.0
+
+dec⟶recomputable = dec⇒recomputable
+{-# WARNING_ON_USAGE dec⟶recomputable
+"Warning: dec⟶recomputable was deprecated in v2.0.
+Please use dec⇒recomputable instead."
+#-}