diff --git a/CHANGELOG.md b/CHANGELOG.md
index 5a42872be0..23d77ad4a7 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -682,6 +682,7 @@ Non-backwards compatible changes
   - `¬-reflects` has been moved from `Relation.Nullary.Negation.Core` to `Relation.Nullary.Reflects`.
   - `decidable-stable`, `excluded-middle` and `¬-drop-Dec` have been moved from `Relation.Nullary.Negation`
     to `Relation.Nullary.Decidable`.
+  - `excluded-middle` has been deprecated in favour of `¬¬-excluded-middle` 
   - `fromDec` and `toDec` have been moved from `Data.Sum.Base` to `Data.Sum`.
 
 ### Refactoring of the unindexed Functor/Applicative/Monad hierarchy
@@ -958,9 +959,6 @@ Non-backwards compatible changes
     lookup : All P xs → (∀ {x} → x ∈ₚ xs → P x)
     lookupₛ : P Respects _≈_ → All P xs → (∀ {x} → x ∈ xs → P x)
     ```
-  * `excluded-middle` in `Relation.Nullary.Decidable.Core` has been renamed to
-    `¬¬-excluded-middle`.
-
 Major improvements
 ------------------
 
@@ -1542,6 +1540,11 @@ Deprecated names
   invPreorder   ↦ converse-preorder
   ```
 
+* In `Relation.Nullary.Decidable.Core`:
+  ```
+  excluded-middle`  ↦  `¬¬-excluded-middle`
+  ```
+
 ### Renamed Data.Erased to Data.Irrelevant
 
 * This fixes the fact we had picked the wrong name originally. The erased modality
@@ -2406,8 +2409,8 @@ Additions to existing modules
   _!≢0    : NonZero (n !)
   _!*_!≢0 : NonZero (m ! * n !)
 
-  anyUpTo? : ∀ (P? : U.Decidable P) (v : ℕ) → Dec (∃ λ n → n < v × P n)
-  allUpTo? : ∀ (P? : U.Decidable P) (v : ℕ) → Dec (∀ {n} → n < v → P n)
+  anyUpTo? : ∀ (P? : Decidable P) (v : ℕ) → Dec (∃ λ n → n < v × P n)
+  allUpTo? : ∀ (P? : Decidable P) (v : ℕ) → Dec (∀ {n} → n < v → P n)
 
   n≤1⇒n≡0∨n≡1 : n ≤ 1 → n ≡ 0 ⊎ n ≡ 1
 
@@ -2921,6 +2924,16 @@ Additions to existing modules
   subst₂-removable : subst₂ _∼_ eq₁ eq₂ p ≅ p
   ```
 
+* Added new constructor for `Relation.Nullary.Decidable`
+  ```
+  T? : ∀ b → Dec (T b)
+  ```
+
+* Added new constructor for `Relation.Nullary.Reflects`
+  ```
+  T⁺ : ∀ b → Reflects (T b) b
+  ```
+
 * Added new definitions in `Relation.Unary`:
   ```
   _≐_  : Pred A ℓ₁ → Pred A ℓ₂ → Set _
diff --git a/README/Axiom.agda b/README/Axiom.agda
index 43805af9c5..c60e08d207 100644
--- a/README/Axiom.agda
+++ b/README/Axiom.agda
@@ -31,7 +31,7 @@ private variable ℓ : Level
 -- The types for which `P` or `¬P` holds is called `Dec P` in the
 -- standard library (short for `Decidable`).
 
-open import Relation.Nullary.Decidable using (Dec)
+open import Relation.Nullary.Decidable.Core using (Dec)
 
 -- The type of the proof of saying that excluded middle holds for
 -- all types at universe level ℓ is therefore:
diff --git a/README/Data/Trie/NonDependent.agda b/README/Data/Trie/NonDependent.agda
index 0484e6005a..e70c378ae5 100644
--- a/README/Data/Trie/NonDependent.agda
+++ b/README/Data/Trie/NonDependent.agda
@@ -64,7 +64,7 @@ open import Data.These       as These
 open import Function.Base using (case_of_; _$_; _∘′_; id; _on_)
 open import Relation.Nary
 open import Relation.Binary.Core using (Rel)
-open import Relation.Nullary.Decidable using (¬?)
+open import Relation.Nullary.Decidable.Core using (¬?)
 
 open import Data.Trie Char.<-strictTotalOrder
 open import Data.Tree.AVL.Value
diff --git a/README/Design/Decidability.agda b/README/Design/Decidability.agda
index c6f086424f..e81e7e98ca 100644
--- a/README/Design/Decidability.agda
+++ b/README/Design/Decidability.agda
@@ -8,7 +8,7 @@
 
 module README.Design.Decidability where
 
-open import Data.Bool
+open import Data.Bool.Base
 open import Data.List.Base using (List; []; _∷_)
 open import Data.List.Properties using (∷-injective)
 open import Data.Nat
@@ -43,7 +43,7 @@ ex₂ true  = ofʸ tt
 ------------------------------------------------------------------------
 -- Dec
 
-open import Relation.Nullary.Decidable
+open import Relation.Nullary.Decidable.Core
 
 -- A proof of `Dec P` is a proof of `Reflects P b` for some `b`.
 -- `Dec P` is declared as a record, with fields:
diff --git a/README/Foreign/Haskell.agda b/README/Foreign/Haskell.agda
index 38c6c78c4e..9b2db72679 100644
--- a/README/Foreign/Haskell.agda
+++ b/README/Foreign/Haskell.agda
@@ -24,7 +24,7 @@ open import Data.List.Base as List using (List; _∷_; []; takeWhile; dropWhile)
 open import Data.Maybe.Base using (Maybe; just; nothing)
 open import Data.Product.Base using (_×_; _,_)
 open import Function
-open import Relation.Nullary.Decidable
+open import Relation.Nullary.Decidable.Core using (¬?)
 
 import Foreign.Haskell as FFI
 open import Foreign.Haskell.Coerce
diff --git a/README/Text/Regex.agda b/README/Text/Regex.agda
index 17d3fe45f9..a099f1cbab 100644
--- a/README/Text/Regex.agda
+++ b/README/Text/Regex.agda
@@ -12,8 +12,7 @@ open import Data.Bool using (true; false)
 open import Data.List.Base using (_∷_; [])
 open import Data.String
 open import Function.Base using () renaming (_$′_ to _$_)
-open import Relation.Nullary.Decidable using (yes)
-open import Relation.Nullary.Decidable using (True; False; from-yes)
+open import Relation.Nullary.Decidable.Core using (yes; True; False; from-yes)
 
 -- Our library available via the Text.Regex module is safe but it works on
 -- lists of characters.
diff --git a/src/Algebra/Construct/LexProduct/Inner.agda b/src/Algebra/Construct/LexProduct/Inner.agda
index 9b6e06f0e6..ac40a4299a 100644
--- a/src/Algebra/Construct/LexProduct/Inner.agda
+++ b/src/Algebra/Construct/LexProduct/Inner.agda
@@ -12,8 +12,8 @@ open import Data.Product.Base using (_×_; _,_; swap; map; uncurry′)
 open import Function.Base using (_∘_)
 open import Level using (Level; _⊔_)
 open import Relation.Binary.Definitions using (Decidable)
-open import Relation.Nullary.Decidable using (does; yes; no)
-open import Relation.Nullary.Negation
+open import Relation.Nullary.Decidable.Core using (does; yes; no)
+open import Relation.Nullary.Negation.Core
   using (contradiction; contradiction₂)
 import Relation.Binary.Reasoning.Setoid as SetoidReasoning
 
diff --git a/src/Algebra/Properties/CancellativeCommutativeSemiring.agda b/src/Algebra/Properties/CancellativeCommutativeSemiring.agda
index e92fa5170e..25cfe832db 100644
--- a/src/Algebra/Properties/CancellativeCommutativeSemiring.agda
+++ b/src/Algebra/Properties/CancellativeCommutativeSemiring.agda
@@ -10,8 +10,8 @@ open import Algebra using (CancellativeCommutativeSemiring)
 open import Algebra.Definitions using (AlmostRightCancellative)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Relation.Binary.Definitions using (Decidable)
-open import Relation.Nullary.Decidable using (yes; no)
-open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Nullary.Decidable.Core using (yes; no)
+open import Relation.Nullary.Negation.Core using (contradiction)
 
 module Algebra.Properties.CancellativeCommutativeSemiring
   {a ℓ} (R : CancellativeCommutativeSemiring a ℓ)
diff --git a/src/Algebra/Solver/CommutativeMonoid.agda b/src/Algebra/Solver/CommutativeMonoid.agda
index 7e4b14b18c..ecca06739b 100644
--- a/src/Algebra/Solver/CommutativeMonoid.agda
+++ b/src/Algebra/Solver/CommutativeMonoid.agda
@@ -28,7 +28,7 @@ import Relation.Nullary.Decidable as Dec
 import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise
 
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
-open import Relation.Nullary.Decidable using (Dec)
+open import Relation.Nullary.Decidable.Core using (Dec)
 
 open CommutativeMonoid M
 open EqReasoning setoid
diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda
index fdba81a838..982f60bd32 100644
--- a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda
+++ b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda
@@ -26,7 +26,7 @@ import Relation.Nullary.Decidable            as Dec
 import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise
 
 open import Relation.Binary.PropositionalEquality as P using (_≡_; decSetoid)
-open import Relation.Nullary.Decidable using (Dec)
+open import Relation.Nullary.Decidable.Core using (Dec)
 
 module Algebra.Solver.IdempotentCommutativeMonoid
   {m₁ m₂} (M : IdempotentCommutativeMonoid m₁ m₂) where
diff --git a/src/Algebra/Solver/Monoid.agda b/src/Algebra/Solver/Monoid.agda
index f80a2847f6..2aa099a57a 100644
--- a/src/Algebra/Solver/Monoid.agda
+++ b/src/Algebra/Solver/Monoid.agda
@@ -24,8 +24,7 @@ open import Relation.Binary.Definitions using (Decidable)
 
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 import Relation.Binary.Reflection
-open import Relation.Nullary
-import Relation.Nullary.Decidable as Dec
+open import Relation.Nullary.Decidable.Core using (map′)
 
 open Monoid M
 open import Relation.Binary.Reasoning.Setoid setoid
@@ -115,7 +114,7 @@ open module R = Relation.Binary.Reflection
 infix 5 _≟_
 
 _≟_ : ∀ {n} → Decidable {A = Normal n} _≡_
-nf₁ ≟ nf₂ = Dec.map′ ≋⇒≡ ≡⇒≋ (nf₁ ≋? nf₂)
+nf₁ ≟ nf₂ = map′ ≋⇒≡ ≡⇒≋ (nf₁ ≋? nf₂)
   where open ListEq Fin._≟_
 
 -- We can also give a sound, but not necessarily complete, procedure
diff --git a/src/Algebra/Solver/Ring.agda b/src/Algebra/Solver/Ring.agda
index 50c191903b..fe18b8e9e6 100644
--- a/src/Algebra/Solver/Ring.agda
+++ b/src/Algebra/Solver/Ring.agda
@@ -39,7 +39,7 @@ open import Algebra.Morphism
 open _-Raw-AlmostCommutative⟶_ morphism renaming (⟦_⟧ to ⟦_⟧′)
 open import Algebra.Properties.Semiring.Exp semiring
 
-open import Relation.Nullary.Decidable using (yes; no)
+open import Relation.Nullary.Decidable.Core using (yes; no)
 open import Relation.Binary.Reasoning.Setoid setoid
 import Relation.Binary.PropositionalEquality.Core as PropEq
 import Relation.Binary.Reflection as Reflection
diff --git a/src/Axiom/DoubleNegationElimination.agda b/src/Axiom/DoubleNegationElimination.agda
index 777f08c017..d427328c1e 100644
--- a/src/Axiom/DoubleNegationElimination.agda
+++ b/src/Axiom/DoubleNegationElimination.agda
@@ -12,7 +12,7 @@ open import Axiom.ExcludedMiddle
 open import Level
 open import Relation.Nullary
 open import Relation.Nullary.Negation
-open import Relation.Nullary.Decidable
+open import Relation.Nullary.Decidable.Core
 
 ------------------------------------------------------------------------
 -- Definition
diff --git a/src/Codata/Musical/Colist.agda b/src/Codata/Musical/Colist.agda
index 21dde992bc..94f741136f 100644
--- a/src/Codata/Musical/Colist.agda
+++ b/src/Codata/Musical/Colist.agda
@@ -35,9 +35,8 @@ import Relation.Binary.Reasoning.Preorder as PreR
 import Relation.Binary.Reasoning.PartialOrder as POR
 open import Relation.Binary.PropositionalEquality as P using (_≡_)
 open import Relation.Nullary.Reflects using (invert)
-open import Relation.Nullary
 open import Relation.Nullary.Negation
-open import Relation.Nullary.Decidable using (¬¬-excluded-middle)
+open import Relation.Nullary.Decidable.Core using (Dec; _because_; ¬¬-excluded-middle)
 open import Relation.Unary using (Pred)
 
 private
diff --git a/src/Codata/Sized/Cofin/Literals.agda b/src/Codata/Sized/Cofin/Literals.agda
index 0995ad4d23..898993d67c 100644
--- a/src/Codata/Sized/Cofin/Literals.agda
+++ b/src/Codata/Sized/Cofin/Literals.agda
@@ -13,7 +13,7 @@ open import Agda.Builtin.FromNat
 open import Codata.Sized.Conat
 open import Codata.Sized.Conat.Properties
 open import Codata.Sized.Cofin
-open import Relation.Nullary.Decidable
+open import Relation.Nullary.Decidable.Core using (True; toWitness)
 
 number : ∀ n → Number (Cofin n)
 number n = record
diff --git a/src/Codata/Sized/Conat/Properties.agda b/src/Codata/Sized/Conat/Properties.agda
index 54e211dc1f..6bc873c6bf 100644
--- a/src/Codata/Sized/Conat/Properties.agda
+++ b/src/Codata/Sized/Conat/Properties.agda
@@ -15,7 +15,7 @@ open import Codata.Sized.Conat
 open import Codata.Sized.Conat.Bisimilarity
 open import Function.Base using (_∋_)
 open import Relation.Nullary
-open import Relation.Nullary.Decidable using (map′)
+open import Relation.Nullary.Decidable.Core using (map′)
 open import Relation.Binary.Definitions using (Decidable)
 
 private
diff --git a/src/Data/Bool.agda b/src/Data/Bool.agda
index 1270125254..55ed146e2c 100644
--- a/src/Data/Bool.agda
+++ b/src/Data/Bool.agda
@@ -8,9 +8,6 @@
 
 module Data.Bool where
 
-open import Relation.Nullary
-open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
-
 ------------------------------------------------------------------------
 -- The boolean type and some operations
 
diff --git a/src/Data/Bool/Properties.agda b/src/Data/Bool/Properties.agda
index 0449279a7d..489ac89fd2 100644
--- a/src/Data/Bool/Properties.agda
+++ b/src/Data/Bool/Properties.agda
@@ -28,8 +28,7 @@ open import Relation.Binary.Definitions
   using (Decidable; Reflexive; Transitive; Antisymmetric; Minimum; Maximum; Total; Irrelevant; Irreflexive; Asymmetric; Trans; Trichotomous; tri≈; tri<; tri>; _Respects₂_)
 open import Relation.Binary.PropositionalEquality.Core
 open import Relation.Binary.PropositionalEquality.Properties
-open import Relation.Nullary.Reflects using (ofʸ; ofⁿ)
-open import Relation.Nullary.Decidable.Core using (True; does; proof; yes; no)
+open import Relation.Nullary.Decidable.Core as Dec using (True; yes; no)
 import Relation.Unary as U
 
 open import Algebra.Definitions {A = Bool} _≡_
@@ -759,9 +758,7 @@ T-irrelevant : U.Irrelevant T
 T-irrelevant {true}  _  _  = refl
 
 T? : U.Decidable T
-does  (T? b) = b
-proof (T? true ) = ofʸ _
-proof (T? false) = ofⁿ λ()
+T? = Dec.T?
 
 T?-diag : ∀ b → T b → True (T? b)
 T?-diag true  _ = _
diff --git a/src/Data/Char/Properties.agda b/src/Data/Char/Properties.agda
index 970eb6249a..1fc2d7e275 100644
--- a/src/Data/Char/Properties.agda
+++ b/src/Data/Char/Properties.agda
@@ -16,7 +16,7 @@ open import Data.Product.Base using (_,_)
 
 open import Function.Base
 open import Relation.Nullary using (¬_; yes; no)
-open import Relation.Nullary.Decidable using (map′; isYes)
+open import Relation.Nullary.Decidable.Core using (map′; isYes)
 open import Relation.Binary.Core using (_⇒_)
 open import Relation.Binary.Bundles
   using (Setoid; DecSetoid; StrictPartialOrder; StrictTotalOrder; Preorder; Poset; DecPoset)
diff --git a/src/Data/Digit.agda b/src/Data/Digit.agda
index 60557b142a..9bbd3cb779 100644
--- a/src/Data/Digit.agda
+++ b/src/Data/Digit.agda
@@ -19,7 +19,7 @@ open import Data.Product.Base using (∃; _,_)
 open import Data.Vec.Base as Vec using (Vec; _∷_; [])
 open import Data.Nat.DivMod
 open import Data.Nat.Induction
-open import Relation.Nullary.Decidable using (True; does; toWitness)
+open import Relation.Nullary.Decidable.Core using (True; does; toWitness)
 open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; refl)
 open import Function.Base using (_$_)
diff --git a/src/Data/Digit/Properties.agda b/src/Data/Digit/Properties.agda
index 113bdde6ca..fb52d2af72 100644
--- a/src/Data/Digit/Properties.agda
+++ b/src/Data/Digit/Properties.agda
@@ -15,7 +15,7 @@ open import Data.Product.Base using (_,_; proj₁)
 open import Data.Vec.Relation.Unary.Unique.Propositional using (Unique)
 import Data.Vec.Relation.Unary.Unique.Propositional.Properties as Uniqueₚ
 open import Data.Vec.Relation.Unary.AllPairs using (allPairs?)
-open import Relation.Nullary.Decidable using (True; from-yes; ¬?)
+open import Relation.Nullary.Decidable.Core using (True; from-yes; ¬?)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 open import Function.Base using (_∘_)
 
diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda
index 2d5b0f638e..0f16a3a752 100644
--- a/src/Data/Fin/Base.agda
+++ b/src/Data/Fin/Base.agda
@@ -17,11 +17,10 @@ open import Data.Product.Base as Product using (_×_; _,_; proj₁; proj₂)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Function.Base using (id; _∘_; _on_; flip)
 open import Level using (0ℓ)
-open import Relation.Nullary.Negation.Core using (contradiction)
-open import Relation.Nullary.Decidable.Core using (yes; no; True; toWitness)
 open import Relation.Binary.Core
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; cong)
 open import Relation.Binary.Indexed.Heterogeneous.Core using (IRel)
+open import Relation.Nullary.Negation.Core using (contradiction)
 
 private
   variable
diff --git a/src/Data/Fin/Induction.agda b/src/Data/Fin/Induction.agda
index a15287a48f..154173d284 100644
--- a/src/Data/Fin/Induction.agda
+++ b/src/Data/Fin/Induction.agda
@@ -31,8 +31,8 @@ import Relation.Binary.Construct.NonStrictToStrict as ToStrict
 import Relation.Binary.Construct.On as On
 open import Relation.Binary.Definitions using (Tri; tri<; tri≈; tri>)
 open import Relation.Binary.PropositionalEquality
-open import Relation.Nullary.Decidable using (yes; no)
-open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Nullary.Decidable.Core using (yes; no)
+open import Relation.Nullary.Negation.Core using (contradiction)
 open import Relation.Unary using (Pred)
 
 module Data.Fin.Induction where
diff --git a/src/Data/Fin/Literals.agda b/src/Data/Fin/Literals.agda
index 3fc30955ba..ae1c04ec57 100644
--- a/src/Data/Fin/Literals.agda
+++ b/src/Data/Fin/Literals.agda
@@ -9,12 +9,12 @@
 module Data.Fin.Literals where
 
 open import Agda.Builtin.FromNat
-open import Data.Nat using (suc; _≤?_)
+open import Data.Nat using (_<?_)
 open import Data.Fin using (Fin ; #_)
-open import Relation.Nullary.Decidable using (True)
+open import Relation.Nullary.Decidable.Core using (True)
 
 number : ∀ n → Number (Fin n)
 number n = record
-  { Constraint = λ m → True (suc m ≤? n)
+  { Constraint = λ m → True (m <? n)
   ; fromNat    = λ m {{pr}} → (# m) {n} {pr}
   }
diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index ef2073269f..e4c3ea03ac 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -43,10 +43,11 @@ open import Relation.Binary.Structures
   using (IsDecEquivalence; IsPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder; IsStrictPartialOrder; IsStrictTotalOrder)
 open import Relation.Binary.PropositionalEquality as P
   using (_≡_; _≢_; refl; sym; trans; cong; cong₂; subst; _≗_; module ≡-Reasoning)
-open import Relation.Nullary
-  using (Reflects; ofʸ; ofⁿ; Dec; _because_; does; proof; yes; no; ¬_; _×-dec_; _⊎-dec_; contradiction)
-open import Relation.Nullary.Reflects
-open import Relation.Nullary.Decidable as Dec using (map′)
+open import Relation.Nullary.Decidable.Core
+  using (Dec; _because_; does; yes; no; _×-dec_; _⊎-dec_; map′)
+open import Relation.Nullary.Decidable using (via-injection)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
+open import Relation.Nullary.Reflects using (invert)
 open import Relation.Unary as U
   using (U; Pred; Decidable; _⊆_; Satisfiable; Universal)
 open import Relation.Unary.Properties using (U?)
@@ -952,7 +953,7 @@ decFinSubset {suc n} {P = P} {Q} Q? P?
 
 any? : ∀ {p} {P : Pred (Fin n) p} → Decidable P → Dec (∃ P)
 any? {zero}  {P = _} P? = no λ { (() , _) }
-any? {suc n} {P = P} P? = Dec.map ⊎⇔∃ (P? zero ⊎-dec any? (P? ∘ suc))
+any? {suc n} {P = P} P? = map′ [ ∃-here , ∃-there ] ∃-toSum (P? zero ⊎-dec any? (P? ∘ suc))
 
 all? : ∀ {p} {P : Pred (Fin n) p} → Decidable P → Dec (∀ f → P f)
 all? P? = map′ (λ ∀p f → ∀p tt) (λ ∀p {x} _ → ∀p x)
@@ -1052,7 +1053,7 @@ module _ {ℓ} {S : Setoid a ℓ} (inj : Injection S (≡-setoid n)) where
   open Setoid S
 
   inj⇒≟ : B.Decidable _≈_
-  inj⇒≟ = Dec.via-injection inj _≟_
+  inj⇒≟ = via-injection inj _≟_
 
   inj⇒decSetoid : DecSetoid a ℓ
   inj⇒decSetoid = record
diff --git a/src/Data/Fin/Show.agda b/src/Data/Fin/Show.agda
index 8f9ae0583b..490c080fa1 100644
--- a/src/Data/Fin/Show.agda
+++ b/src/Data/Fin/Show.agda
@@ -14,8 +14,7 @@ open import Data.Nat as ℕ using (ℕ; _≤?_; _<?_)
 import Data.Nat.Show as ℕ using (show; readMaybe)
 open import Data.String.Base using (String)
 open import Function.Base
-open import Relation.Nullary.Decidable using (yes; no)
-open import Relation.Nullary.Decidable using (True)
+open import Relation.Nullary.Decidable.Core using (yes; no; True)
 
 show : ∀ {n} → Fin n → String
 show = ℕ.show ∘′ toℕ
diff --git a/src/Data/Fin/Subset/Properties.agda b/src/Data/Fin/Subset/Properties.agda
index 2f7246da6a..9d313e5d4c 100644
--- a/src/Data/Fin/Subset/Properties.agda
+++ b/src/Data/Fin/Subset/Properties.agda
@@ -37,8 +37,8 @@ open import Relation.Binary.Bundles
   using (Preorder; Poset; StrictPartialOrder; DecStrictPartialOrder)
 open import Relation.Binary.Definitions as B hiding (Decidable)
 open import Relation.Binary.PropositionalEquality
-open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _⊎-dec_)
-open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Nullary.Decidable.Core using (Dec; yes; no; _⊎-dec_; map′)
+open import Relation.Nullary.Negation.Core using (contradiction)
 open import Relation.Unary using (Pred; Decidable; Satisfiable)
 
 private
@@ -110,7 +110,7 @@ infix 4 _∈?_
 _∈?_ : ∀ x (p : Subset n) → Dec (x ∈ p)
 zero  ∈? inside  ∷ p = yes here
 zero  ∈? outside ∷ p = no  λ()
-suc n ∈? s       ∷ p = Dec.map′ there drop-there (n ∈? p)
+suc n ∈? s       ∷ p = map′ there drop-there (n ∈? p)
 
 ------------------------------------------------------------------------
 -- Empty
@@ -225,9 +225,9 @@ x∉⁅y⁆⇒x≢y x∉⁅x⁆ refl = x∉⁅x⁆ (x∈⁅x⁆ _)
 infix 4 _⊆?_
 _⊆?_ : B.Decidable {A = Subset n} _⊆_
 []          ⊆? []          = yes id
-outside ∷ p ⊆?       y ∷ q = Dec.map out⊆-⇔ (p ⊆? q)
+outside ∷ p ⊆?       y ∷ q = map′ out⊆ drop-∷-⊆ (p ⊆? q)
 inside  ∷ p ⊆? outside ∷ q = no (λ p⊆q → case (p⊆q here) of λ())
-inside  ∷ p ⊆? inside  ∷ q = Dec.map in⊆in-⇔ (p ⊆? q)
+inside  ∷ p ⊆? inside  ∷ q = map′ in⊆in drop-∷-⊆ (p ⊆? q)
 
 module _ (n : ℕ) where
 
@@ -290,10 +290,10 @@ infix 4 _⊂?_
 
 _⊂?_ : B.Decidable {A = Subset n} _⊂_
 []          ⊂? []          = no λ ()
-outside ∷ p ⊂? outside ∷ q = Dec.map out⊂out-⇔ (p ⊂? q)
-outside ∷ p ⊂? inside  ∷ q = Dec.map out⊂in-⇔ (p ⊆? q)
+outside ∷ p ⊂? outside ∷ q = map′ out⊂ drop-∷-⊂ (p ⊂? q)
+outside ∷ p ⊂? inside  ∷ q = map′ out⊂in (drop-∷-⊆ ∘ proj₁) (p ⊆? q)
 inside  ∷ p ⊂? outside ∷ q = no (λ {(p⊆q , _) → case (p⊆q here) of λ ()})
-inside  ∷ p ⊂? inside  ∷ q = Dec.map in⊂in-⇔ (p ⊂? q)
+inside  ∷ p ⊂? inside  ∷ q = map′ in⊂in drop-∷-⊂ (p ⊂? q)
 
 module _ (n : ℕ) where
 
@@ -856,8 +856,10 @@ module _ {P : Pred (Subset (suc n)) ℓ} where
     ∃-Subset-suc
 
 anySubset? : ∀ {P : Pred (Subset n) ℓ} → Decidable P → Dec ∃⟨ P ⟩
-anySubset? {n = zero}  P? = Dec.map ∃-Subset-[]-⇔ (P? [])
-anySubset? {n = suc n} P? = Dec.map ∃-Subset-∷-⇔
+anySubset? {n = zero}  P? = map′ ([] ,_) ∃-Subset-zero (P? [])
+anySubset? {n = suc n} P? = map′
+  [ Product.map _ id , Product.map _ id ]′
+  ∃-Subset-suc
   (anySubset? (P? ∘ (inside ∷_)) ⊎-dec anySubset? (P? ∘ (outside ∷_)))
 
 
diff --git a/src/Data/Float/Properties.agda b/src/Data/Float/Properties.agda
index a397dd53ec..ab02a26eba 100644
--- a/src/Data/Float/Properties.agda
+++ b/src/Data/Float/Properties.agda
@@ -16,7 +16,7 @@ import Data.Nat.Properties as Nₚ
 import Data.Word.Base as Word
 import Data.Word.Properties as Wₚ
 open import Function.Base using (_∘_)
-open import Relation.Nullary.Decidable as RN using (map′)
+open import Relation.Nullary.Decidable.Core using (map′)
 open import Relation.Binary.Core using (_⇒_)
 open import Relation.Binary.Bundles using (Setoid; DecSetoid)
 open import Relation.Binary.Structures
diff --git a/src/Data/Integer/DivMod.agda b/src/Data/Integer/DivMod.agda
index 87bbaabbe7..4c2846f160 100644
--- a/src/Data/Integer/DivMod.agda
+++ b/src/Data/Integer/DivMod.agda
@@ -15,7 +15,6 @@ import Data.Nat.Properties as ℕ
 import Data.Nat.DivMod as ℕ
 import Data.Sign as S
 open import Function.Base using (_∘′_)
-open import Relation.Nullary.Decidable
 open import Relation.Binary.PropositionalEquality
 
 open ≤-Reasoning
diff --git a/src/Data/Integer/Divisibility/Signed.agda b/src/Data/Integer/Divisibility/Signed.agda
index af06d57486..2972804ae6 100644
--- a/src/Data/Integer/Divisibility/Signed.agda
+++ b/src/Data/Integer/Divisibility/Signed.agda
@@ -28,8 +28,7 @@ open import Relation.Binary.Definitions
   using (Reflexive; Transitive; Decidable)
 open import Relation.Binary.PropositionalEquality
 import Relation.Binary.Reasoning.Preorder as PreorderReasoning
-open import Relation.Nullary.Decidable using (yes; no)
-import Relation.Nullary.Decidable as DEC
+open import Relation.Nullary.Decidable.Core using (yes; no; map′)
 
 ------------------------------------------------------------------------
 -- Type
@@ -134,7 +133,7 @@ module ∣-Reasoning where
 infix 4 _∣?_
 
 _∣?_ : Decidable _∣_
-k ∣? m = DEC.map′ ∣ᵤ⇒∣ ∣⇒∣ᵤ (∣ k ∣ ℕ.∣? ∣ m ∣)
+k ∣? m = map′ ∣ᵤ⇒∣ ∣⇒∣ᵤ (∣ k ∣ ℕ.∣? ∣ m ∣)
 
 0∣⇒≡0 : ∀ {m} → 0ℤ ∣ m → m ≡ 0ℤ
 0∣⇒≡0 0|m = ∣i∣≡0⇒i≡0 (ℕ.0∣⇒≡0 (∣⇒∣ᵤ 0|m))
diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda
index 5760b050ec..1427e800d8 100644
--- a/src/Data/Integer/Properties.agda
+++ b/src/Data/Integer/Properties.agda
@@ -35,10 +35,9 @@ open import Relation.Binary.Structures
 open import Relation.Binary.Definitions
   using (DecidableEquality; Reflexive; Transitive; Antisymmetric; Total; Decidable; Irrelevant; Irreflexive; Asymmetric; Trans; Trichotomous; tri≈; tri<; tri>)
 open import Relation.Binary.PropositionalEquality
-open import Relation.Nullary using (yes; no; ¬_)
-import Relation.Nullary.Reflects as Reflects
-open import Relation.Nullary.Negation using (contradiction)
-import Relation.Nullary.Decidable as Dec
+open import Relation.Nullary.Decidable.Core using (yes; no; map′)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
+open import Relation.Nullary.Reflects using (invert)
 
 open import Algebra.Definitions {A = ℤ} _≡_
 open import Algebra.Consequences.Propositional
@@ -68,10 +67,10 @@ private
 
 infix 4 _≟_
 _≟_ : DecidableEquality ℤ
-+ m      ≟ + n      = Dec.map′ (cong (+_)) +-injective (m ℕ.≟ n)
++ m      ≟ + n      = map′ (cong (+_)) +-injective (m ℕ.≟ n)
 + m      ≟ -[1+ n ] = no λ()
 -[1+ m ] ≟ + n      = no λ()
--[1+ m ] ≟ -[1+ n ] = Dec.map′ (cong -[1+_]) -[1+-injective (m ℕ.≟ n)
+-[1+ m ] ≟ -[1+ n ] = map′ (cong -[1+_]) -[1+-injective (m ℕ.≟ n)
 
 ≡-setoid : Setoid 0ℓ 0ℓ
 ≡-setoid = setoid ℤ
@@ -117,10 +116,10 @@ drop‿-≤- (-≤- n≤m) = n≤m
 
 infix  4 _≤?_
 _≤?_ : Decidable _≤_
--[1+ m ] ≤? -[1+ n ] = Dec.map′ -≤- drop‿-≤- (n ℕ.≤? m)
+-[1+ m ] ≤? -[1+ n ] = map′ -≤- drop‿-≤- (n ℕ.≤? m)
 -[1+ m ] ≤? +    n   = yes -≤+
 +    m   ≤? -[1+ n ] = no λ ()
-+    m   ≤? +    n   = Dec.map′ +≤+ drop‿+≤+ (m ℕ.≤? n)
++    m   ≤? +    n   = map′ +≤+ drop‿+≤+ (m ℕ.≤? n)
 
 ≤-irrelevant : Irrelevant _≤_
 ≤-irrelevant -≤+       -≤+         = refl
@@ -308,10 +307,10 @@ drop‿-<- (-<- n<m) = n<m
 
 infix 4 _<?_
 _<?_ : Decidable _<_
--[1+ m ] <? -[1+ n ] = Dec.map′ -<- drop‿-<- (n ℕ.<? m)
+-[1+ m ] <? -[1+ n ] = map′ -<- drop‿-<- (n ℕ.<? m)
 -[1+ m ] <? + n      = yes -<+
 + m      <? -[1+ n ] = no λ()
-+ m      <? + n      = Dec.map′ +<+ drop‿+<+ (m ℕ.<? n)
++ m      <? + n      = map′ +<+ drop‿+<+ (m ℕ.<? n)
 
 <-irrelevant : Irrelevant _<_
 <-irrelevant (-<- n<m₁) (-<- n<m₂) = cong -<- (ℕ.<-irrelevant n<m₁ n<m₂)
@@ -613,7 +612,7 @@ n⊖n≡0 n with n ℕ.<ᵇ n in leq
   - (suc n ⊖ suc m) ∎ where open ≡-Reasoning
 
 ⊖-≥ : m ℕ.≥ n → m ⊖ n ≡ + (m ∸ n)
-⊖-≥ {m} {n} p with m ℕ.<ᵇ n | Reflects.invert (ℕ.<ᵇ-reflects-< m n)
+⊖-≥ {m} {n} p with m ℕ.<ᵇ n | invert (ℕ.<ᵇ-reflects-< m n)
 ... | true  | q = contradiction (ℕ.<-transʳ p q) (ℕ.<-irrefl refl)
 ... | false | q = refl
 
@@ -626,7 +625,7 @@ n⊖n≡0 n with n ℕ.<ᵇ n in leq
   + (suc n ∸ suc m) ∎ where open ≡-Reasoning
 
 ⊖-≤ : m ℕ.≤ n → m ⊖ n ≡ - + (n ∸ m)
-⊖-≤ {m} {n} p with m ℕ.<ᵇ n | Reflects.invert (ℕ.<ᵇ-reflects-< m n)
+⊖-≤ {m} {n} p with m ℕ.<ᵇ n | invert (ℕ.<ᵇ-reflects-< m n)
 ... | true  | q = refl
 ... | false | q rewrite ℕ.≤-antisym p (ℕ.≮⇒≥ q) | ℕ.n∸n≡0 n = refl
 
@@ -664,7 +663,7 @@ m-n≡m⊖n (suc m) zero    = cong +[1+_] (ℕ.+-identityʳ m)
 m-n≡m⊖n (suc m) (suc n) = refl
 
 -[n⊖m]≡-m+n : ∀ m n → - (m ⊖ n) ≡ (- (+ m)) + (+ n)
--[n⊖m]≡-m+n m n with m ℕ.<ᵇ n | Reflects.invert (ℕ.<ᵇ-reflects-< m n)
+-[n⊖m]≡-m+n m n with m ℕ.<ᵇ n | invert (ℕ.<ᵇ-reflects-< m n)
 ... | true  | p = begin
   - (- (+ (n ∸ m))) ≡⟨ neg-involutive (+ (n ∸ m)) ⟩
   + (n ∸ m)         ≡˘⟨ ⊖-≥ (ℕ.≤-trans (ℕ.m≤n+m m 1) p) ⟩
diff --git a/src/Data/List/Fresh/Relation/Unary/All.agda b/src/Data/List/Fresh/Relation/Unary/All.agda
index 2f560e82c2..8b71a84fa4 100644
--- a/src/Data/List/Fresh/Relation/Unary/All.agda
+++ b/src/Data/List/Fresh/Relation/Unary/All.agda
@@ -11,7 +11,7 @@ module Data.List.Fresh.Relation.Unary.All where
 open import Level using (Level; _⊔_; Lift)
 open import Data.Product.Base using (_×_; _,_; proj₁; uncurry)
 open import Data.Sum.Base as Sum using (inj₁; inj₂)
-open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _×-dec_)
+open import Relation.Nullary.Decidable.Core using (Dec; yes; no; map′; _×-dec_)
 open import Relation.Unary  as U
 open import Relation.Binary.Core using (Rel)
 
@@ -65,7 +65,7 @@ module _ {R : Rel A r} {P : Pred A p} (P? : Decidable P) where
 
   all? : (xs : List# A R) → Dec (All P xs)
   all? []        = yes []
-  all? (x ∷# xs) = Dec.map′ (uncurry _∷_) uncons (P? x ×-dec all? xs)
+  all? (x ∷# xs) = map′ (uncurry _∷_) uncons (P? x ×-dec all? xs)
 
 ------------------------------------------------------------------------
 -- Generalised decidability procedure
diff --git a/src/Data/List/Fresh/Relation/Unary/Any.agda b/src/Data/List/Fresh/Relation/Unary/Any.agda
index dbb9dd0dec..c77154f040 100644
--- a/src/Data/List/Fresh/Relation/Unary/Any.agda
+++ b/src/Data/List/Fresh/Relation/Unary/Any.agda
@@ -13,8 +13,8 @@ open import Data.Empty
 open import Data.Product.Base using (∃; _,_; -,_)
 open import Data.Sum.Base using (_⊎_; [_,_]′; inj₁; inj₂)
 open import Function.Bundles using (_⇔_; mk⇔)
-open import Relation.Nullary.Negation using (¬_)
-open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _⊎-dec_)
+open import Relation.Nullary.Negation.Core using (¬_)
+open import Relation.Nullary.Decidable.Core using (Dec; yes; no; _⊎-dec_; map′)
 open import Relation.Unary  as U
 open import Relation.Binary.Core using (Rel)
 
@@ -79,4 +79,4 @@ module _ {R : Rel A r} {P : Pred A p} (P? : Decidable P) where
 
   any? : (xs : List# A R) → Dec (Any P xs)
   any? []        = no (λ ())
-  any? (x ∷# xs) = Dec.map ⊎⇔Any (P? x ⊎-dec any? xs)
+  any? (x ∷# xs) = map′ fromSum toSum (P? x ⊎-dec any? xs)
diff --git a/src/Data/List/Membership/DecSetoid.agda b/src/Data/List/Membership/DecSetoid.agda
index 8f34aab9f6..6299c9dd2b 100644
--- a/src/Data/List/Membership/DecSetoid.agda
+++ b/src/Data/List/Membership/DecSetoid.agda
@@ -8,7 +8,7 @@
 
 open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Binary.Bundles using (DecSetoid)
-open import Relation.Nullary.Decidable using (¬?)
+open import Relation.Nullary.Decidable.Core using (¬?)
 
 module Data.List.Membership.DecSetoid {a ℓ} (DS : DecSetoid a ℓ) where
 
diff --git a/src/Data/List/Membership/Propositional/Properties.agda b/src/Data/List/Membership/Propositional/Properties.agda
index 06240c6be5..6b1e71097b 100644
--- a/src/Data/List/Membership/Propositional/Properties.agda
+++ b/src/Data/List/Membership/Propositional/Properties.agda
@@ -40,11 +40,9 @@ open import Relation.Binary.PropositionalEquality as P
   using (_≡_; _≢_; refl; sym; trans; cong; subst; →-to-⟶; _≗_)
 import Relation.Binary.Properties.DecTotalOrder as DTOProperties
 open import Relation.Unary using (_⟨×⟩_; Decidable)
-import Relation.Nullary.Reflects as Reflects
+open import Relation.Nullary.Decidable.Core using (Dec; does; yes; no; ¬¬-excluded-middle)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Nullary.Reflects using (invert)
-open import Relation.Nullary using (¬_; Dec; does; yes; no; _because_)
-open import Relation.Nullary.Negation using (contradiction)
-open import Relation.Nullary.Decidable using (¬¬-excluded-middle)
 
 private
   open module ListMonad {ℓ} = RawMonad (monad {ℓ = ℓ})
@@ -373,13 +371,14 @@ finite inj (x ∷ xs) fᵢ∈x∷xs = ¬¬-excluded-middle helper
     lemma i≤j i≰1+j refl = i≰1+j (m≤n⇒m≤1+n i≤j)
 
     f′ⱼ∈xs : ∀ j → f′ j ∈ xs
-    f′ⱼ∈xs j with i ≤ᵇ j | Reflects.invert (≤ᵇ-reflects-≤ i j)
+    f′ⱼ∈xs j with i ≤ᵇ j | invert (≤ᵇ-reflects-≤ i j)
     ... | true  | p = ∈-if-not-i (<⇒≢ (s≤s p))
     ... | false | p = ∈-if-not-i (<⇒≢ (≰⇒> p) ∘ sym)
 
+
     f′-injective′ : Injective _≡_ _≡_ f′
-    f′-injective′ {j} {k} eq with i ≤ᵇ j | Reflects.invert (≤ᵇ-reflects-≤ i j)
-                                | i ≤ᵇ k | Reflects.invert (≤ᵇ-reflects-≤ i k)
+    f′-injective′ {j} {k} eq with i ≤ᵇ j | invert (≤ᵇ-reflects-≤ i j)
+                                | i ≤ᵇ k | invert (≤ᵇ-reflects-≤ i k)
     ... | true  | p | true  | q = P.cong pred (f-inj eq)
     ... | true  | p | false | q = contradiction (f-inj eq) (lemma p q)
     ... | false | p | true  | q = contradiction (f-inj eq) (lemma q p ∘ sym)
diff --git a/src/Data/List/Membership/Setoid.agda b/src/Data/List/Membership/Setoid.agda
index 1b8a67fb7d..419df3508e 100644
--- a/src/Data/List/Membership/Setoid.agda
+++ b/src/Data/List/Membership/Setoid.agda
@@ -12,12 +12,12 @@ open import Relation.Binary.Definitions using (_Respects_)
 module Data.List.Membership.Setoid {c ℓ} (S : Setoid c ℓ) where
 
 open import Function.Base using (_∘_; id; flip)
-open import Data.List.Base as List using (List; []; _∷_; length; lookup)
+open import Data.List.Base as List using (List; []; _∷_)
 open import Data.List.Relation.Unary.Any
   using (Any; index; map; here; there)
 open import Data.Product.Base as Prod using (∃; _×_; _,_)
 open import Relation.Unary using (Pred)
-open import Relation.Nullary.Negation using (¬_)
+open import Relation.Nullary.Negation.Core using (¬_)
 
 open Setoid S renaming (Carrier to A)
 
diff --git a/src/Data/List/Membership/Setoid/Properties.agda b/src/Data/List/Membership/Setoid/Properties.agda
index 1a74ace45f..e7ff18a71d 100644
--- a/src/Data/List/Membership/Setoid/Properties.agda
+++ b/src/Data/List/Membership/Setoid/Properties.agda
@@ -32,10 +32,9 @@ open import Relation.Binary.Definitions as B hiding (Decidable)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 open import Relation.Unary as U using (Decidable; Pred)
-open import Relation.Nullary using (¬_; does; _because_; yes; no)
+open import Relation.Nullary.Decidable.Core using (does; _because_; ¬?)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Nullary.Reflects using (invert)
-open import Relation.Nullary.Negation using (contradiction)
-open import Relation.Nullary.Decidable using (¬?)
 open Setoid using (Carrier)
 
 private
diff --git a/src/Data/List/NonEmpty/Base.agda b/src/Data/List/NonEmpty/Base.agda
index 82f16c270a..6b38ded501 100644
--- a/src/Data/List/NonEmpty/Base.agda
+++ b/src/Data/List/NonEmpty/Base.agda
@@ -22,7 +22,7 @@ open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; _≢_; refl)
 open import Relation.Unary using (Pred; Decidable; U; ∅)
 open import Relation.Unary.Properties using (U?; ∅?)
-open import Relation.Nullary.Decidable using (does)
+open import Relation.Nullary.Decidable.Core using (does)
 
 private
   variable
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index eb403f8b91..c203ea6e54 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -38,9 +38,10 @@ open import Relation.Binary.Definitions as B using (DecidableEquality)
 import Relation.Binary.Reasoning.Setoid as EqR
 open import Relation.Binary.PropositionalEquality as P hiding ([_])
 open import Relation.Binary.Core using (Rel)
+open import Relation.Nullary.Decidable.Core
+  using (Dec; does; _because_; yes; no; map′; ¬?; _×-dec_)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Nullary.Reflects using (invert)
-open import Relation.Nullary using (¬_; Dec; does; _because_; yes; no; contradiction)
-open import Relation.Nullary.Decidable as Decidable using (isYes; map′; ⌊_⌋; ¬?; _×-dec_)
 open import Relation.Unary using (Pred; Decidable; ∁)
 open import Relation.Unary.Properties using (∁?)
 
@@ -71,7 +72,7 @@ module _ {x y : A} {xs ys : List A} where
   ∷-injectiveʳ refl = refl
 
   ∷-dec : Dec (x ≡ y) → Dec (xs ≡ ys) → Dec (x List.∷ xs ≡ y ∷ ys)
-  ∷-dec x≟y xs≟ys = Decidable.map′ (uncurry (cong₂ _∷_)) ∷-injective (x≟y ×-dec xs≟ys)
+  ∷-dec x≟y xs≟ys = map′ (uncurry (cong₂ _∷_)) ∷-injective (x≟y ×-dec xs≟ys)
 
 ≡-dec : DecidableEquality A → DecidableEquality (List A)
 ≡-dec _≟_ []       []       = yes refl
diff --git a/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda
index 9af0162ded..0a9c585663 100644
--- a/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda
+++ b/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda
@@ -17,8 +17,8 @@ import Data.Nat.Properties as ℕₚ
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Function.Base using (case_of_; _$′_)
 
-open import Relation.Nullary.Decidable using (yes; no; does; map′; _⊎-dec_)
-open import Relation.Nullary.Negation using (¬_; contradiction)
+open import Relation.Nullary.Decidable.Core using (yes; no; does; map′; _⊎-dec_)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Unary as U using (Pred)
 open import Relation.Binary.Core using (REL; _⇒_)
 open import Relation.Binary.Definitions using (Decidable; Trans; Antisym)
diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
index ce16a7528a..d46ffd6c57 100644
--- a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
@@ -41,8 +41,8 @@ import Relation.Binary.Reasoning.Setoid as RelSetoid
 open import Relation.Binary.Properties.Setoid S using (≉-resp₂)
 open import Relation.Binary.PropositionalEquality.Core as ≡
   using (_≡_ ; refl; sym; cong; cong₂; subst; _≢_)
-open import Relation.Nullary.Decidable using (yes; no; does)
-open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Nullary.Decidable.Core using (yes; no; does)
+open import Relation.Nullary.Negation.Core using (contradiction)
 
 private
   variable
diff --git a/src/Data/List/Relation/Binary/Pointwise.agda b/src/Data/List/Relation/Binary/Pointwise.agda
index 2728418ddc..a69375d0bb 100644
--- a/src/Data/List/Relation/Binary/Pointwise.agda
+++ b/src/Data/List/Relation/Binary/Pointwise.agda
@@ -23,7 +23,6 @@ open import Data.Nat.Base using (ℕ; zero; suc)
 open import Data.Nat.Properties
 open import Level
 open import Relation.Nullary hiding (Irrelevant)
-import Relation.Nullary.Decidable as Dec using (map′)
 open import Relation.Unary as U using (Pred)
 open import Relation.Binary.Core renaming (Rel to Rel₂)
 open import Relation.Binary.Definitions using (_Respects_; _Respects₂_)
diff --git a/src/Data/List/Relation/Binary/Pointwise/Properties.agda b/src/Data/List/Relation/Binary/Pointwise/Properties.agda
index 7dfba09296..5b45e9ab54 100644
--- a/src/Data/List/Relation/Binary/Pointwise/Properties.agda
+++ b/src/Data/List/Relation/Binary/Pointwise/Properties.agda
@@ -14,8 +14,7 @@ open import Level
 open import Relation.Binary.Core using (REL; _⇒_)
 open import Relation.Binary.Definitions
 import Relation.Binary.PropositionalEquality.Core as P
-open import Relation.Nullary using (yes; no; _×-dec_)
-import Relation.Nullary.Decidable as Dec
+open import Relation.Nullary.Decidable.Core using (yes; no; map′; _×-dec_)
 
 open import Data.List.Relation.Binary.Pointwise.Base
 
@@ -68,7 +67,7 @@ decidable : Decidable R → Decidable (Pointwise R)
 decidable _  []       []       = yes []
 decidable _  []       (y ∷ ys) = no λ()
 decidable _  (x ∷ xs) []       = no λ()
-decidable R? (x ∷ xs) (y ∷ ys) = Dec.map′ (uncurry _∷_) uncons
+decidable R? (x ∷ xs) (y ∷ ys) = map′ (uncurry _∷_) uncons
   (R? x y ×-dec decidable R? xs ys)
 
 irrelevant : Irrelevant R → Irrelevant (Pointwise R)
diff --git a/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda
index 202bff89b0..ee71f3c4d5 100644
--- a/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda
+++ b/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda
@@ -22,8 +22,8 @@ open import Data.Nat.Properties using (suc-injective)
 open import Data.Product.Base as Prod using (_×_; _,_; proj₁; proj₂; uncurry)
 open import Function.Base
 
-open import Relation.Nullary.Negation using (¬_)
-open import Relation.Nullary.Decidable as Dec using (_×-dec_; yes; no; _because_)
+open import Relation.Nullary.Negation.Core using (¬_)
+open import Relation.Nullary.Decidable.Core using (_×-dec_; yes; no; _because_; map′)
 open import Relation.Unary as U using (Pred)
 open import Relation.Binary.Core using (Rel; REL; _⇒_)
 open import Relation.Binary.Definitions
@@ -218,5 +218,5 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
   prefix? : Decidable R → Decidable (Prefix R)
   prefix? R? []       bs       = yes []
   prefix? R? (a ∷ as) []       = no (λ ())
-  prefix? R? (a ∷ as) (b ∷ bs) = Dec.map′ (uncurry _∷_) uncons
+  prefix? R? (a ∷ as) (b ∷ bs) = map′ (uncurry _∷_) uncons
                                $ R? a b ×-dec prefix? R? as bs
diff --git a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda
index b11e011d76..e787b19098 100644
--- a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda
+++ b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda
@@ -29,9 +29,9 @@ open import Data.Product.Base using (∃₂; _×_; _,_; <_,_>; proj₂; uncurry)
 open import Function.Base
 open import Function.Bundles using (_⤖_; _⇔_ ; mk⤖; mk⇔)
 open import Function.Consequences.Propositional using (strictlySurjective⇒surjective)
+open import Relation.Nullary.Decidable.Core using (Dec; does; _because_; yes; no; map′; ¬?)
+open import Relation.Nullary.Negation.Core using (¬_)
 open import Relation.Nullary.Reflects using (invert)
-open import Relation.Nullary using (Dec; does; _because_; yes; no; ¬_)
-open import Relation.Nullary.Decidable as Dec using (¬?)
 open import Relation.Unary as U using (Pred)
 open import Relation.Binary.Core using (Rel; REL; _⇒_)
 open import Relation.Binary.Bundles using (Preorder; Poset; DecPoset)
@@ -417,9 +417,9 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} (R? : Decidable R) wher
   sublist? (x ∷ xs) []       = no λ ()
   sublist? (x ∷ xs) (y ∷ ys) with R? x y
   ... | true  because  [r] =
-    Dec.map (∷⁻¹  (invert  [r])) (sublist? xs ys)
+    map′ ((invert  [r]) ∷_) ∷⁻ (sublist? xs ys)
   ... | false because [¬r] =
-    Dec.map (∷ʳ⁻¹ (invert [¬r])) (sublist? (x ∷ xs) ys)
+    map′ (_ ∷ʳ_) (∷ʳ⁻ (invert [¬r])) (sublist? (x ∷ xs) ys)
 
 module _ {a e r} {A : Set a} {E : Rel A e} {R : Rel A r} where
 
@@ -496,12 +496,12 @@ module Disjointness {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
   ⊆-disjoint? (x≈z ∷ τ₁) (y≈z ∷ τ₂) = no λ()
   -- Present in either sublist: ok.
   ⊆-disjoint? (y ∷ʳ τ₁) (x≈y ∷ τ₂) =
-    Dec.map′ (x≈y ∷ᵣ_) (λ{ (_ ∷ᵣ d) → d }) (⊆-disjoint? τ₁ τ₂)
+    map′ (x≈y ∷ᵣ_) (λ{ (_ ∷ᵣ d) → d }) (⊆-disjoint? τ₁ τ₂)
   ⊆-disjoint? (x≈y ∷ τ₁) (y ∷ʳ τ₂) =
-    Dec.map′ (x≈y ∷ₗ_) (λ{ (_ ∷ₗ d) → d }) (⊆-disjoint? τ₁ τ₂)
+    map′ (x≈y ∷ₗ_) (λ{ (_ ∷ₗ d) → d }) (⊆-disjoint? τ₁ τ₂)
   -- Present in neither sublist: ok.
   ⊆-disjoint? (y ∷ʳ τ₁) (.y ∷ʳ τ₂) =
-    Dec.map′ (y ∷ₙ_) (λ{ (_ ∷ₙ d) → d }) (⊆-disjoint? τ₁ τ₂)
+    map′ (y ∷ₙ_) (λ{ (_ ∷ₙ d) → d }) (⊆-disjoint? τ₁ τ₂)
 
   -- Disjoint is proof-irrelevant
 
diff --git a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
index 19fe765456..412f3efd97 100644
--- a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
@@ -25,8 +25,8 @@ open import Relation.Binary.Definitions using () renaming (Decidable to Decidabl
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
 open import Relation.Binary.Structures using (IsDecTotalOrder)
 open import Relation.Unary using (Pred; Decidable; Irrelevant)
-open import Relation.Nullary.Negation using (¬_)
-open import Relation.Nullary.Decidable using (¬?; yes; no)
+open import Relation.Nullary.Negation.Core using (¬_)
+open import Relation.Nullary.Decidable.Core using (¬?; yes; no)
 
 import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality
 import Data.List.Relation.Binary.Sublist.Setoid as SetoidSublist
diff --git a/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda
index 3ea10495e6..b60b19d040 100644
--- a/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda
+++ b/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda
@@ -20,15 +20,14 @@ open import Data.List.Relation.Binary.Prefix.Heterogeneous as Prefix
 open import Data.Nat.Base
 open import Data.Nat.Properties
 open import Function.Base using (_$_; flip)
-open import Relation.Nullary using (Dec; does; ¬_)
-import Relation.Nullary.Decidable as Dec
-open import Relation.Unary as U using (Pred)
-open import Relation.Nullary.Negation using (contradiction)
 open import Relation.Binary.Core using (REL; Rel; _⇒_)
 open import Relation.Binary.Definitions as B
   using (Trans; Antisym; Irrelevant)
 open import Relation.Binary.PropositionalEquality.Core as P
   using (_≡_; _≢_; refl; sym; subst; subst₂)
+open import Relation.Nullary.Decidable.Core using (does; map′)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
+open import Relation.Unary as U using (Pred)
 
 import Data.List.Properties as Listₚ
 import Data.List.Relation.Binary.Prefix.Heterogeneous.Properties as Prefixₚ
@@ -208,5 +207,5 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
 -- Decidability
 
   suffix? : B.Decidable R → B.Decidable (Suffix R)
-  suffix? R? as bs = Dec.map′ fromPrefix-rev toPrefix-rev
+  suffix? R? as bs = map′ fromPrefix-rev toPrefix-rev
                    $ Prefixₚ.prefix? R? (reverse as) (reverse bs)
diff --git a/src/Data/List/Relation/Ternary/Interleaving/Setoid/Properties.agda b/src/Data/List/Relation/Ternary/Interleaving/Setoid/Properties.agda
index 936bca38b4..3805ec26e1 100644
--- a/src/Data/List/Relation/Ternary/Interleaving/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Ternary/Interleaving/Setoid/Properties.agda
@@ -14,8 +14,7 @@ module Data.List.Relation.Ternary.Interleaving.Setoid.Properties
 open import Data.List.Base using (List; []; _∷_; filter; _++_)
 open import Data.Bool.Base using (true; false)
 open import Relation.Unary using (Decidable)
-open import Relation.Nullary.Decidable using (does)
-open import Relation.Nullary.Decidable using (¬?)
+open import Relation.Nullary.Decidable.Core using (does; ¬?)
 open import Function.Base using (_∘_)
 
 open import Data.List.Relation.Binary.Equality.Setoid S using (≋-refl)
diff --git a/src/Data/List/Relation/Unary/All.agda b/src/Data/List/Relation/Unary/All.agda
index 97da349699..c36aa8caed 100644
--- a/src/Data/List/Relation/Unary/All.agda
+++ b/src/Data/List/Relation/Unary/All.agda
@@ -20,8 +20,7 @@ open import Data.Product.Base as Prod
 open import Data.Sum.Base as Sum using (inj₁; inj₂)
 open import Function.Base using (_∘_; _∘′_; id; const)
 open import Level using (Level; _⊔_)
-open import Relation.Nullary hiding (Irrelevant)
-import Relation.Nullary.Decidable as Dec
+open import Relation.Nullary.Decidable.Core using (yes; map′; _×-dec_)
 open import Relation.Unary hiding (_∈_)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Definitions using (_Respects_)
@@ -206,7 +205,7 @@ module _(S : Setoid a ℓ) {P : Pred (Setoid.Carrier S) p} where
 
 all? : Decidable P → Decidable (All P)
 all? p []       = yes []
-all? p (x ∷ xs) = Dec.map′ (uncurry _∷_) uncons (p x ×-dec all? p xs)
+all? p (x ∷ xs) = map′ (uncurry _∷_) uncons (p x ×-dec all? p xs)
 
 universal : Universal P → Universal (All P)
 universal u []       = []
diff --git a/src/Data/List/Relation/Unary/All/Properties.agda b/src/Data/List/Relation/Unary/All/Properties.agda
index 6af4fd2a8c..ece9851742 100644
--- a/src/Data/List/Relation/Unary/All/Properties.agda
+++ b/src/Data/List/Relation/Unary/All/Properties.agda
@@ -42,8 +42,8 @@ open import Relation.Binary.PropositionalEquality
   using (_≡_; refl; cong; cong₂; _≗_)
 open import Relation.Nullary
 open import Relation.Nullary.Reflects using (invert)
-open import Relation.Nullary.Negation using (contradiction)
-open import Relation.Nullary.Decidable using (¬?; decidable-stable)
+open import Relation.Nullary.Negation.Core using (contradiction)
+open import Relation.Nullary.Decidable.Core using (¬?; decidable-stable)
 open import Relation.Unary
   using (Decidable; Pred; Universal; ∁; _∩_; _⟨×⟩_) renaming (_⊆_ to _⋐_)
 open import Relation.Unary.Properties using (∁?)
diff --git a/src/Data/List/Relation/Unary/AllPairs.agda b/src/Data/List/Relation/Unary/AllPairs.agda
index bed4a5972d..5ef27ad5fd 100644
--- a/src/Data/List/Relation/Unary/AllPairs.agda
+++ b/src/Data/List/Relation/Unary/AllPairs.agda
@@ -20,7 +20,7 @@ open import Relation.Binary.Definitions as B
 open import Relation.Binary.Construct.Intersection renaming (_∩_ to _∩ᵇ_)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Unary as U renaming (_∩_ to _∩ᵘ_) hiding (_⇒_)
-open import Relation.Nullary.Decidable as Dec using (_×-dec_; yes; no)
+open import Relation.Nullary.Decidable.Core using (_×-dec_; yes; no; map′)
 
 ------------------------------------------------------------------------
 -- Definition
@@ -69,7 +69,7 @@ module _ {s} {S : Rel A s} where
 allPairs? : B.Decidable R → U.Decidable (AllPairs R)
 allPairs? R? []       = yes []
 allPairs? R? (x ∷ xs) =
-  Dec.map′ (uncurry _∷_) uncons (All.all? (R? x) xs ×-dec allPairs? R? xs)
+  map′ (uncurry _∷_) uncons (All.all? (R? x) xs ×-dec allPairs? R? xs)
 
 irrelevant : B.Irrelevant R → U.Irrelevant (AllPairs R)
 irrelevant irr []           []           = refl
diff --git a/src/Data/List/Relation/Unary/AllPairs/Properties.agda b/src/Data/List/Relation/Unary/AllPairs/Properties.agda
index c116fcb00f..581150a4eb 100644
--- a/src/Data/List/Relation/Unary/AllPairs/Properties.agda
+++ b/src/Data/List/Relation/Unary/AllPairs/Properties.agda
@@ -23,7 +23,7 @@ open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Bundles using (DecSetoid)
 open import Relation.Binary.PropositionalEquality.Core using (_≢_)
 open import Relation.Unary using (Pred; Decidable)
-open import Relation.Nullary.Decidable using (does)
+open import Relation.Nullary.Decidable.Core using (does)
 
 private
   variable
diff --git a/src/Data/List/Relation/Unary/Any.agda b/src/Data/List/Relation/Unary/Any.agda
index eb010e2a39..a45a69ac72 100644
--- a/src/Data/List/Relation/Unary/Any.agda
+++ b/src/Data/List/Relation/Unary/Any.agda
@@ -14,9 +14,8 @@ open import Data.List.Base as List using (List; []; [_]; _∷_)
 open import Data.Product.Base as Prod using (∃; _,_)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Level using (Level; _⊔_)
-open import Relation.Nullary using (¬_; yes; no; _⊎-dec_)
-import Relation.Nullary.Decidable as Dec
-open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Nullary.Decidable.Core using (yes; no; map′; _⊎-dec_)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Unary hiding (_∈_)
 
 private
@@ -90,7 +89,7 @@ fromSum (inj₂ pxs) = there pxs
 
 any? : Decidable P → Decidable (Any P)
 any? P? []       = no λ()
-any? P? (x ∷ xs) = Dec.map′ fromSum toSum (P? x ⊎-dec any? P? xs)
+any? P? (x ∷ xs) = map′ fromSum toSum (P? x ⊎-dec any? P? xs)
 
 satisfiable : Satisfiable P → Satisfiable (Any P)
 satisfiable (x , Px) = [ x ] , here Px
diff --git a/src/Data/List/Relation/Unary/Any/Properties.agda b/src/Data/List/Relation/Unary/Any/Properties.agda
index aba1a777ee..14efe8edc3 100644
--- a/src/Data/List/Relation/Unary/Any/Properties.agda
+++ b/src/Data/List/Relation/Unary/Any/Properties.agda
@@ -45,9 +45,9 @@ open import Relation.Binary.PropositionalEquality.Core as P
   using (_≡_; refl)
 open import Relation.Unary as U
   using (Pred; _⟨×⟩_; _⟨→⟩_) renaming (_⊆_ to _⋐_)
-open import Relation.Nullary using (¬_; _because_; does; ofʸ; ofⁿ; yes; no)
-open import Relation.Nullary.Decidable using (¬?; decidable-stable)
-open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Nullary.Decidable.Core using (does; _because_; yes; no; ¬?; decidable-stable)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
+open import Relation.Nullary.Reflects using (invert)
 
 private
   open module ListMonad {ℓ} = RawMonad (monad {ℓ = ℓ})
@@ -521,8 +521,8 @@ module _ (Q? : U.Decidable Q) where
 
   filter⁺ : (p : Any P xs) → Any P (filter Q? xs) ⊎ ¬ Q (Any.lookup p)
   filter⁺ {xs = x ∷ _} (here px) with Q? x
-  ... | true  because _       = inj₁ (here px)
-  ... | false because ofⁿ ¬Qx = inj₂ ¬Qx
+  ... | true  because _     = inj₁ (here px)
+  ... | false because [¬Qx] = inj₂ (invert [¬Qx])
   filter⁺ {xs = x ∷ _} (there p) with does (Q? x)
   ... | true  = Sum.map₁ there (filter⁺ p)
   ... | false = filter⁺ p
@@ -542,8 +542,8 @@ module _ {R : A → A → Set r} (R? : B.Decidable R) where
     derun⁺-aux : ∀ x xs → P Respects R → P x → Any P (derun R? (x ∷ xs))
     derun⁺-aux x [] resp Px = here Px
     derun⁺-aux x (y ∷ xs) resp Px with R? x y
-    ... | true  because ofʸ Rxy = derun⁺-aux y xs resp (resp Rxy Px)
-    ... | false because _       = here Px
+    ... | true  because [Rxy] = derun⁺-aux y xs resp (resp (invert [Rxy]) Px)
+    ... | false because _     = here Px
 
   derun⁺ : P Respects R → Any P xs → Any P (derun R? xs)
   derun⁺ {xs = x ∷ xs}     resp (here px)   = derun⁺-aux x xs resp px
diff --git a/src/Data/List/Relation/Unary/Grouped.agda b/src/Data/List/Relation/Unary/Grouped.agda
index f10bc1fd32..e9e32d39d1 100644
--- a/src/Data/List/Relation/Unary/Grouped.agda
+++ b/src/Data/List/Relation/Unary/Grouped.agda
@@ -16,7 +16,7 @@ open import Relation.Binary.Core using (REL; Rel)
 open import Relation.Binary.Definitions as B
 open import Relation.Unary as U using (Pred)
 open import Relation.Nullary.Negation using (¬_)
-open import Relation.Nullary.Decidable as Dec using (yes; ¬?; _⊎-dec_; _×-dec_)
+open import Relation.Nullary.Decidable.Core using (yes; map′; ¬?; _⊎-dec_; _×-dec_)
 open import Level using (Level; _⊔_)
 
 private
@@ -45,7 +45,7 @@ module _ {_≈_ : Rel A ℓ} where
   grouped? _≟_ [] = yes []
   grouped? _≟_ (x ∷ []) = yes ([] ∷≉ [])
   grouped? _≟_ (x ∷ y ∷ xs) =
-    Dec.map′ from to ((x ≟ y ⊎-dec all? (λ z → ¬? (x ≟ z)) (y ∷ xs)) ×-dec (grouped? _≟_ (y ∷ xs)))
+    map′ from to ((x ≟ y ⊎-dec all? (λ z → ¬? (x ≟ z)) (y ∷ xs)) ×-dec (grouped? _≟_ (y ∷ xs)))
     where
     from : ((x ≈ y) ⊎ All (λ z → ¬ (x ≈ z)) (y ∷ xs)) × Grouped _≈_ (y ∷ xs) → Grouped _≈_ (x ∷ y ∷ xs)
     from (inj₁ x≈y          , grouped[y∷xs]) = x≈y          ∷≈ grouped[y∷xs]
diff --git a/src/Data/List/Relation/Unary/Linked.agda b/src/Data/List/Relation/Unary/Linked.agda
index 38fcdd1507..ebf399716d 100644
--- a/src/Data/List/Relation/Unary/Linked.agda
+++ b/src/Data/List/Relation/Unary/Linked.agda
@@ -21,7 +21,7 @@ open import Relation.Binary.Core using (Rel; _⇒_)
 open import Relation.Binary.Construct.Intersection renaming (_∩_ to _∩ᵇ_)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Unary as U renaming (_∩_ to _∩ᵘ_) hiding (_⇒_)
-open import Relation.Nullary.Decidable using (yes; no; map′; _×-dec_)
+open import Relation.Nullary.Decidable.Core using (yes; no; map′; _×-dec_)
 
 private
   variable
diff --git a/src/Data/List/Relation/Unary/Linked/Properties.agda b/src/Data/List/Relation/Unary/Linked/Properties.agda
index 10ece2fdb3..a0a918b701 100644
--- a/src/Data/List/Relation/Unary/Linked/Properties.agda
+++ b/src/Data/List/Relation/Unary/Linked/Properties.agda
@@ -27,7 +27,7 @@ open import Relation.Binary.Bundles using (DecSetoid)
 open import Relation.Binary.Definitions using (Transitive)
 open import Relation.Binary.PropositionalEquality.Core using (_≢_)
 open import Relation.Unary using (Pred; Decidable)
-open import Relation.Nullary.Decidable using (yes; no; does)
+open import Relation.Nullary.Decidable.Core using (yes; no; does)
 
 private
   variable
diff --git a/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda b/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda
index c8c4210ed6..9bfb6100c3 100644
--- a/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda
+++ b/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda
@@ -27,7 +27,7 @@ open import Relation.Binary.Core using (_Preserves_⟶_)
 open import Relation.Binary.Bundles using (TotalOrder; DecTotalOrder; Preorder)
 import Relation.Binary.Properties.TotalOrder as TotalOrderProperties
 open import Relation.Unary using (Pred; Decidable)
-open import Relation.Nullary.Decidable using (yes; no)
+open import Relation.Nullary.Decidable.Core using (yes; no)
 
 private
   variable
diff --git a/src/Data/List/Relation/Unary/Unique/DecSetoid.agda b/src/Data/List/Relation/Unary/Unique/DecSetoid.agda
index bddc7b2727..e5f3245d4e 100644
--- a/src/Data/List/Relation/Unary/Unique/DecSetoid.agda
+++ b/src/Data/List/Relation/Unary/Unique/DecSetoid.agda
@@ -9,7 +9,7 @@
 open import Relation.Binary.Bundles using (DecSetoid)
 import Data.List.Relation.Unary.AllPairs as AllPairs
 open import Relation.Unary using (Decidable)
-open import Relation.Nullary.Decidable using (¬?)
+open import Relation.Nullary.Decidable.Core using (¬?)
 
 module Data.List.Relation.Unary.Unique.DecSetoid
   {a ℓ} (DS : DecSetoid a ℓ) where
diff --git a/src/Data/List/Relation/Unary/Unique/DecSetoid/Properties.agda b/src/Data/List/Relation/Unary/Unique/DecSetoid/Properties.agda
index 9e97527ff8..d7d7bb3375 100644
--- a/src/Data/List/Relation/Unary/Unique/DecSetoid/Properties.agda
+++ b/src/Data/List/Relation/Unary/Unique/DecSetoid/Properties.agda
@@ -12,7 +12,7 @@ open import Data.List.Relation.Unary.All.Properties using (all-filter)
 open import Data.List.Relation.Unary.Unique.Setoid.Properties
 open import Level
 open import Relation.Binary.Bundles using (DecSetoid)
-open import Relation.Nullary.Decidable using (¬?)
+open import Relation.Nullary.Decidable.Core using (¬?)
 
 module Data.List.Relation.Unary.Unique.DecSetoid.Properties where
 
diff --git a/src/Data/List/Sort/MergeSort.agda b/src/Data/List/Sort/MergeSort.agda
index 9648718d0d..77510731a4 100644
--- a/src/Data/List/Sort/MergeSort.agda
+++ b/src/Data/List/Sort/MergeSort.agda
@@ -20,14 +20,14 @@ import Data.List.Relation.Unary.All.Properties as All
 open import Data.List.Relation.Binary.Permutation.Propositional
 import Data.List.Relation.Binary.Permutation.Propositional.Properties as Perm
 open import Data.Maybe.Base using (just)
-open import Relation.Nullary.Decidable using (does)
 open import Data.Nat using (_<_; _>_; z<s; s<s)
 open import Data.Nat.Induction
 open import Data.Nat.Properties using (m<n⇒m<1+n)
 open import Data.Product.Base as Prod using (_,_)
 open import Function.Base using (_∘_)
 open import Relation.Binary.Bundles using (DecTotalOrder)
-open import Relation.Nullary.Negation using (¬_)
+open import Relation.Nullary.Decidable.Core using (does)
+open import Relation.Nullary.Negation.Core using (¬_)
 
 module Data.List.Sort.MergeSort
   {a ℓ₁ ℓ₂} (O : DecTotalOrder a ℓ₁ ℓ₂) where
diff --git a/src/Data/Maybe/Base.agda b/src/Data/Maybe/Base.agda
index b0ae001f46..378a252819 100644
--- a/src/Data/Maybe/Base.agda
+++ b/src/Data/Maybe/Base.agda
@@ -16,8 +16,8 @@ open import Data.Unit.Base using (⊤)
 open import Data.These.Base using (These; this; that; these)
 open import Data.Product.Base as Prod using (_×_; _,_)
 open import Function.Base
-open import Relation.Nullary.Reflects
-open import Relation.Nullary.Decidable.Core
+open import Relation.Nullary.Decidable.Core using (Dec; _because_)
+open import Relation.Nullary.Reflects using (invert)
 
 private
   variable
@@ -47,8 +47,8 @@ is-nothing : Maybe A → Bool
 is-nothing = not ∘ is-just
 
 decToMaybe : Dec A → Maybe A
-decToMaybe ( true because [a]) = just (invert [a])
-decToMaybe (false because  _ ) = nothing
+decToMaybe (true  because [a]) = just (invert [a])
+decToMaybe (false because   _) = nothing
 
 -- A dependent eliminator.
 
diff --git a/src/Data/Maybe/Properties.agda b/src/Data/Maybe/Properties.agda
index 4940da433f..37eef3c0c0 100644
--- a/src/Data/Maybe/Properties.agda
+++ b/src/Data/Maybe/Properties.agda
@@ -19,8 +19,7 @@ open import Function.Definitions using (Injective)
 open import Level using (Level)
 open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Binary.PropositionalEquality
-open import Relation.Nullary.Decidable using (yes; no)
-open import Relation.Nullary.Decidable using (map′)
+open import Relation.Nullary.Decidable.Core using (yes; no; map′)
 
 private
   variable
diff --git a/src/Data/Maybe/Relation/Binary/Connected.agda b/src/Data/Maybe/Relation/Binary/Connected.agda
index 8c174c9ea1..d43da64b22 100644
--- a/src/Data/Maybe/Relation/Binary/Connected.agda
+++ b/src/Data/Maybe/Relation/Binary/Connected.agda
@@ -14,8 +14,7 @@ open import Function.Bundles using (_⇔_; mk⇔)
 open import Relation.Binary.Core using (REL; _⇒_)
 open import Relation.Binary.Definitions using (Reflexive; Sym; Decidable)
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
-open import Relation.Nullary
-import Relation.Nullary.Decidable as Dec
+open import Relation.Nullary.Decidable.Core using (yes; map′)
 
 private
   variable
@@ -61,7 +60,7 @@ sym R-sym just-nothing = nothing-just
 sym R-sym nothing      = nothing
 
 connected? : Decidable R → Decidable (Connected R)
-connected? R? (just x) (just y) = Dec.map just-equivalence (R? x y)
+connected? R? (just x) (just y) = map′ just drop-just (R? x y)
 connected? R? (just x) nothing  = yes just-nothing
 connected? R? nothing  (just y) = yes nothing-just
 connected? R? nothing  nothing  = yes nothing
diff --git a/src/Data/Maybe/Relation/Binary/Pointwise.agda b/src/Data/Maybe/Relation/Binary/Pointwise.agda
index 48fa144a2e..5195e3e601 100644
--- a/src/Data/Maybe/Relation/Binary/Pointwise.agda
+++ b/src/Data/Maybe/Relation/Binary/Pointwise.agda
@@ -17,8 +17,7 @@ open import Relation.Binary.Bundles using (Setoid; DecSetoid)
 open import Relation.Binary.Definitions using (Reflexive; Sym; Trans; Decidable)
 open import Relation.Binary.Structures using (IsEquivalence; IsDecEquivalence)
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
-open import Relation.Nullary
-import Relation.Nullary.Decidable as Dec
+open import Relation.Nullary.Decidable.Core using (yes; no; map′)
 
 ------------------------------------------------------------------------
 -- Definition
@@ -75,7 +74,7 @@ module _ {a b c r₁ r₂ r₃} {A : Set a} {B : Set b} {C : Set c}
 module _ {a r} {A : Set a} {R : Rel A r} where
 
   dec : Decidable R → Decidable (Pointwise R)
-  dec R-dec (just x) (just y) = Dec.map just-equivalence (R-dec x y)
+  dec R-dec (just x) (just y) = map′ just drop-just (R-dec x y)
   dec R-dec (just x) nothing  = no (λ ())
   dec R-dec nothing  (just y) = no (λ ())
   dec R-dec nothing  nothing  = yes nothing
diff --git a/src/Data/Maybe/Relation/Unary/All.agda b/src/Data/Maybe/Relation/Unary/All.agda
index c070bd279d..db305095c0 100644
--- a/src/Data/Maybe/Relation/Unary/All.agda
+++ b/src/Data/Maybe/Relation/Unary/All.agda
@@ -18,8 +18,7 @@ open import Function.Bundles using (_⇔_; mk⇔)
 open import Level
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; cong)
 open import Relation.Unary
-open import Relation.Nullary hiding (Irrelevant)
-import Relation.Nullary.Decidable as Dec
+open import Relation.Nullary.Decidable.Core using (yes; map′)
 
 ------------------------------------------------------------------------
 -- Definition
@@ -106,7 +105,7 @@ module _ {a p} {A : Set a} {P : Pred A p} where
 
   dec : Decidable P → Decidable (All P)
   dec P-dec nothing  = yes nothing
-  dec P-dec (just x) = Dec.map just-equivalence (P-dec x)
+  dec P-dec (just x) = map′ just drop-just (P-dec x)
 
   universal : Universal P → Universal (All P)
   universal P-universal (just x) = just (P-universal x)
diff --git a/src/Data/Maybe/Relation/Unary/Any.agda b/src/Data/Maybe/Relation/Unary/Any.agda
index 48cd402ce0..83979f309e 100644
--- a/src/Data/Maybe/Relation/Unary/Any.agda
+++ b/src/Data/Maybe/Relation/Unary/Any.agda
@@ -15,8 +15,7 @@ open import Function.Bundles using (_⇔_; mk⇔)
 open import Level
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; cong)
 open import Relation.Unary
-open import Relation.Nullary hiding (Irrelevant)
-import Relation.Nullary.Decidable as Dec
+open import Relation.Nullary.Decidable.Core as Dec using (no; map′)
 
 ------------------------------------------------------------------------
 -- Definition
@@ -67,7 +66,7 @@ module _ {a p} {A : Set a} {P : Pred A p} where
 
   dec : Decidable P → Decidable (Any P)
   dec P-dec nothing  = no λ ()
-  dec P-dec (just x) = Dec.map just-equivalence (P-dec x)
+  dec P-dec (just x) = map′ just drop-just (P-dec x)
 
   irrelevant : Irrelevant P → Irrelevant (Any P)
   irrelevant P-irrelevant (just p) (just q) = cong just (P-irrelevant p q)
diff --git a/src/Data/Nat/Binary/Properties.agda b/src/Data/Nat/Binary/Properties.agda
index 638482131f..157cf11f83 100644
--- a/src/Data/Nat/Binary/Properties.agda
+++ b/src/Data/Nat/Binary/Properties.agda
@@ -38,9 +38,9 @@ open import Relation.Binary.Consequences
 open import Relation.Binary.Morphism
 import Relation.Binary.Morphism.OrderMonomorphism as OrderMonomorphism
 open import Relation.Binary.PropositionalEquality
-open import Relation.Nullary using (¬_; yes; no)
-import Relation.Nullary.Decidable as Dec
-open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
+import Relation.Binary.Reasoning.Base.Triple as InequalityReasoning
+open import Relation.Nullary.Decidable.Core using (yes; no; map′)
 
 open import Algebra.Definitions {A = ℕᵇ} _≡_
 open import Algebra.Structures {A = ℕᵇ} _≡_
@@ -78,11 +78,11 @@ zero     ≟ zero     =  yes refl
 zero     ≟ 2[1+ _ ] =  no λ()
 zero     ≟ 1+[2 _ ] =  no λ()
 2[1+ _ ] ≟ zero     =  no λ()
-2[1+ x ] ≟ 2[1+ y ] =  Dec.map′ (cong 2[1+_]) 2[1+_]-injective (x ≟ y)
+2[1+ x ] ≟ 2[1+ y ] =  map′ (cong 2[1+_]) 2[1+_]-injective (x ≟ y)
 2[1+ _ ] ≟ 1+[2 _ ] =  no λ()
 1+[2 _ ] ≟ zero     =  no λ()
 1+[2 _ ] ≟ 2[1+ _ ] =  no λ()
-1+[2 x ] ≟ 1+[2 y ] =  Dec.map′ (cong 1+[2_]) 1+[2_]-injective (x ≟ y)
+1+[2 x ] ≟ 1+[2 y ] =  map′ (cong 1+[2_]) 1+[2_]-injective (x ≟ y)
 
 ≡-isDecEquivalence : IsDecEquivalence {A = ℕᵇ} _≡_
 ≡-isDecEquivalence = isDecEquivalence _≟_
diff --git a/src/Data/Nat/Combinatorics/Specification.agda b/src/Data/Nat/Combinatorics/Specification.agda
index 0b263eed54..95a637037d 100644
--- a/src/Data/Nat/Combinatorics/Specification.agda
+++ b/src/Data/Nat/Combinatorics/Specification.agda
@@ -19,8 +19,8 @@ open import Data.Nat.Combinatorics.Base
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Relation.Binary.PropositionalEquality
   using (_≡_; trans; _≢_)
-open import Relation.Nullary.Decidable using (yes; no; does)
-open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Nullary.Decidable.Core using (yes; no)
+open import Relation.Nullary.Negation.Core using (contradiction)
 open import Relation.Binary.PropositionalEquality
   using (subst; refl; sym; cong; cong₂)
 
diff --git a/src/Data/Nat/DivMod.agda b/src/Data/Nat/DivMod.agda
index c879cec098..ea43420f0f 100644
--- a/src/Data/Nat/DivMod.agda
+++ b/src/Data/Nat/DivMod.agda
@@ -19,8 +19,7 @@ open import Data.Nat.Induction
 open import Data.Nat.Properties
 open import Function.Base using (_$_)
 open import Relation.Binary.PropositionalEquality
-open import Relation.Nullary.Decidable using (yes; no)
-open import Relation.Nullary.Decidable using (False; toWitnessFalse)
+open import Relation.Nullary.Decidable.Core using (yes; no)
 
 open ≤-Reasoning
 
diff --git a/src/Data/Nat/DivMod/Core.agda b/src/Data/Nat/DivMod/Core.agda
index 8ada6d77b2..cbe6ab2417 100644
--- a/src/Data/Nat/DivMod/Core.agda
+++ b/src/Data/Nat/DivMod/Core.agda
@@ -16,8 +16,8 @@ open import Data.Nat.Properties
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Data.Product.Base using (_×_; _,_)
 open import Relation.Binary.PropositionalEquality
-open import Relation.Nullary.Decidable using (yes; no)
-open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Nullary.Decidable.Core using (yes; no)
+open import Relation.Nullary.Negation.Core using (contradiction)
 
 open ≤-Reasoning
 
diff --git a/src/Data/Nat/Divisibility.agda b/src/Data/Nat/Divisibility.agda
index ea4814b964..385a2f24b5 100644
--- a/src/Data/Nat/Divisibility.agda
+++ b/src/Data/Nat/Divisibility.agda
@@ -16,7 +16,7 @@ open import Data.Unit.Base using (tt)
 open import Function.Base using (_∘′_; _$_)
 open import Function.Bundles using (_⇔_; mk⇔)
 open import Level using (0ℓ)
-open import Relation.Nullary.Decidable as Dec using (False; yes; no)
+open import Relation.Nullary.Decidable.Core using (yes; no; map′)
 open import Relation.Nullary.Negation.Core using (contradiction)
 open import Relation.Binary.Core using (_⇒_)
 open import Relation.Binary.Bundles using (Preorder; Poset)
@@ -88,7 +88,7 @@ infix 4 _∣?_
 _∣?_ : Decidable _∣_
 zero  ∣? zero   = yes (divides-refl 0)
 zero  ∣? suc m  = no ((λ()) ∘′ ∣-antisym (divides-refl 0))
-suc n ∣? m      = Dec.map (m%n≡0⇔n∣m m (suc n)) (m % suc n ≟ 0)
+n@(suc _) ∣? m  = map′ (m%n≡0⇒n∣m m n) (n∣m⇒m%n≡0 m n) (m % n ≟ 0)
 
 ∣-isPreorder : IsPreorder _≡_ _∣_
 ∣-isPreorder = record
diff --git a/src/Data/Nat/GCD.agda b/src/Data/Nat/GCD.agda
index 2aa87002ca..180d8a516d 100644
--- a/src/Data/Nat/GCD.agda
+++ b/src/Data/Nat/GCD.agda
@@ -24,9 +24,8 @@ open import Induction.Lexicographic using (_⊗_; [_⊗_])
 open import Relation.Binary.Definitions using (tri<; tri>; tri≈; Symmetric)
 open import Relation.Binary.PropositionalEquality.Core as P
   using (_≡_; _≢_; subst; cong)
-open import Relation.Nullary.Decidable using (Dec)
-open import Relation.Nullary.Negation using (contradiction)
-import Relation.Nullary.Decidable as Dec
+open import Relation.Nullary.Decidable.Core using (Dec; map′)
+open import Relation.Nullary.Negation.Core using (contradiction)
 
 open import Algebra.Definitions {A = ℕ} _≡_ as Algebra
   using (Associative; Commutative; LeftIdentity; RightIdentity; LeftZero; RightZero; Zero)
@@ -280,8 +279,8 @@ mkGCD m n = gcd m n , gcd-GCD m n
 
 gcd? : (m n d : ℕ) → Dec (GCD m n d)
 gcd? m n d =
-  Dec.map′ (λ { P.refl → gcd-GCD m n }) (GCD.unique (gcd-GCD m n))
-           (gcd m n ≟ d)
+  map′ (λ { P.refl → gcd-GCD m n }) (GCD.unique (gcd-GCD m n))
+       (gcd m n ≟ d)
 
 GCD-* : ∀ {m n d c} .{{_ : NonZero c}} → GCD (m * c) (n * c) (d * c) → GCD m n d
 GCD-* {c = suc _} (GCD.is (dc∣nc , dc∣mc) dc-greatest) =
diff --git a/src/Data/Nat/LCM.agda b/src/Data/Nat/LCM.agda
index 545870574f..d06cf678fa 100644
--- a/src/Data/Nat/LCM.agda
+++ b/src/Data/Nat/LCM.agda
@@ -19,7 +19,6 @@ open import Data.Product.Base using (_×_; _,_; uncurry′; ∃)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Relation.Binary.PropositionalEquality.Core as P
   using (_≡_; refl; sym; trans; cong; cong₂; module ≡-Reasoning)
-open import Relation.Nullary.Decidable using (False; fromWitnessFalse)
 
 private
   -- instance
diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda
index 8e72b32be0..74f083edef 100644
--- a/src/Data/Nat/Primality.agda
+++ b/src/Data/Nat/Primality.agda
@@ -16,9 +16,9 @@ open import Data.Nat.Properties
 open import Data.Product.Base using (∃; _×_; map₂; _,_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Function.Base using (flip; _∘_; _∘′_)
-open import Relation.Nullary.Decidable as Dec
-  using (yes; no; from-yes; ¬?; decidable-stable; _×-dec_; _→-dec_)
-open import Relation.Nullary.Negation using (¬_; contradiction)
+open import Relation.Nullary.Decidable.Core
+  using (yes; no; from-yes; map′; ¬?; decidable-stable; _×-dec_; _→-dec_)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Unary using (Decidable)
 open import Relation.Binary.PropositionalEquality
   using (refl; cong)
@@ -50,7 +50,7 @@ Prime n = ∀ {d} → 2 ≤ d → d < n → d ∤ n
 composite? : Decidable Composite
 composite? 0               = no λ()
 composite? 1               = no λ()
-composite? n@(suc (suc _)) = Dec.map′
+composite? n@(suc (suc _)) = map′
   (map₂ λ { (a , b , c) → (b , a , c)})
   (map₂ λ { (a , b , c) → (b , a , c)})
   (anyUpTo? (λ d → 2 ≤? d ×-dec d ∣? n) n)
@@ -58,7 +58,7 @@ composite? n@(suc (suc _)) = Dec.map′
 prime? : Decidable Prime
 prime? 0               = no λ()
 prime? 1               = no λ()
-prime? n@(suc (suc _)) = Dec.map′
+prime? n@(suc (suc _)) = map′
   (λ f {d} → flip (f {d}))
   (λ f {d} → flip (f {d}))
   (allUpTo? (λ d → 2 ≤? d →-dec ¬? (d ∣? n)) n)
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 5ed9b64e43..f304416950 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -42,8 +42,8 @@ open import Relation.Binary.Definitions
 open import Relation.Binary.Consequences using (flip-Connex)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary hiding (Irrelevant)
-open import Relation.Nullary.Decidable using (True; via-injection; map′)
-open import Relation.Nullary.Negation using (contradiction; contradiction₂)
+open import Relation.Nullary.Decidable using (via-injection; map′)
+open import Relation.Nullary.Negation.Core using (contradiction; contradiction₂)
 open import Relation.Nullary.Reflects using (fromEquivalence)
 
 open import Algebra.Definitions {A = ℕ} _≡_
diff --git a/src/Data/Nat/Show.agda b/src/Data/Nat/Show.agda
index 23ab91b0fd..959a86386b 100644
--- a/src/Data/Nat/Show.agda
+++ b/src/Data/Nat/Show.agda
@@ -19,7 +19,7 @@ open import Data.Nat
 open import Data.Product.Base using (proj₁)
 open import Data.String.Base using (toList; fromList; String)
 open import Function.Base using (_∘′_; _∘_)
-open import Relation.Nullary.Decidable using (True)
+open import Relation.Nullary.Decidable.Core using (True)
 
 ------------------------------------------------------------------------
 -- Read
diff --git a/src/Data/Nat/Show/Properties.agda b/src/Data/Nat/Show/Properties.agda
index 564264946c..38a68400c6 100644
--- a/src/Data/Nat/Show/Properties.agda
+++ b/src/Data/Nat/Show/Properties.agda
@@ -12,7 +12,7 @@ open import Function.Base using (_∘_)
 import Data.List.Properties as Listₚ
 open import Data.Nat.Base using (ℕ)
 open import Data.Nat.Properties using (_≤?_)
-open import Relation.Nullary.Decidable using (True)
+open import Relation.Nullary.Decidable.Core using (True)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 open import Data.Nat.Show using (charsInBase)
 
diff --git a/src/Data/Product/Properties.agda b/src/Data/Product/Properties.agda
index 5e8509b76e..4496c6c236 100644
--- a/src/Data/Product/Properties.agda
+++ b/src/Data/Product/Properties.agda
@@ -15,7 +15,7 @@ open import Function.Bundles using (_↔_; mk↔ₛ′)
 open import Level using (Level)
 open import Relation.Binary.Definitions using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality
-open import Relation.Nullary.Decidable as Dec using (Dec; yes; no)
+open import Relation.Nullary.Decidable.Core using (Dec; yes; no; map′)
 
 private
   variable
@@ -43,7 +43,7 @@ module _ {B : A → Set b} where
           DecidableEquality (Σ A B)
   ≡-dec dec₁ dec₂ (a , x) (b , y) with dec₁ a b
   ... | no [a≢b] = no ([a≢b] ∘ ,-injectiveˡ)
-  ... | yes refl = Dec.map′ (cong (a ,_)) (,-injectiveʳ-UIP (Decidable⇒UIP.≡-irrelevant dec₁)) (dec₂ x y)
+  ... | yes refl = map′ (cong (a ,_)) (,-injectiveʳ-UIP (Decidable⇒UIP.≡-irrelevant dec₁)) (dec₂ x y)
 
 ------------------------------------------------------------------------
 -- Equality (non-dependent)
diff --git a/src/Data/Product/Relation/Binary/Lex/Strict.agda b/src/Data/Product/Relation/Binary/Lex/Strict.agda
index 742c642d60..3660c39ccb 100644
--- a/src/Data/Product/Relation/Binary/Lex/Strict.agda
+++ b/src/Data/Product/Relation/Binary/Lex/Strict.agda
@@ -19,7 +19,7 @@ open import Data.Empty
 open import Function.Base
 open import Induction.WellFounded
 open import Level
-open import Relation.Nullary.Decidable
+open import Relation.Nullary.Decidable.Core using (_⊎-dec_; _×-dec_)
 open import Relation.Binary.Core using (Rel; _⇒_)
 open import Relation.Binary.Bundles
   using (Preorder; StrictPartialOrder; StrictTotalOrder)
diff --git a/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda b/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda
index efa64a8605..784434d04a 100644
--- a/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda
+++ b/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda
@@ -14,7 +14,7 @@ open import Data.Sum.Base
 open import Data.Unit.Base using (⊤)
 open import Level using (Level; _⊔_; 0ℓ)
 open import Function
-open import Relation.Nullary.Decidable using (_×-dec_)
+open import Relation.Nullary.Decidable.Core using (_×-dec_)
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 import Relation.Binary.PropositionalEquality.Properties as P
diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda
index 959573218a..2742e44ced 100644
--- a/src/Data/Rational/Properties.agda
+++ b/src/Data/Rational/Properties.agda
@@ -59,9 +59,8 @@ open import Relation.Binary.Definitions
 open import Relation.Binary.PropositionalEquality
 open import Relation.Binary.Morphism.Structures
 import Relation.Binary.Morphism.OrderMonomorphism as OrderMonomorphisms
-open import Relation.Nullary.Decidable as Dec
-  using (True; False; fromWitness; fromWitnessFalse; toWitnessFalse; yes; no; recompute; map′; _×-dec_)
-open import Relation.Nullary.Negation using (¬_; contradiction; contraposition)
+open import Relation.Nullary.Decidable.Core using (yes; no; map′; _×-dec_)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction; contraposition)
 
 open import Algebra.Definitions {A = ℚ} _≡_
 open import Algebra.Structures  {A = ℚ} _≡_
@@ -505,7 +504,7 @@ private
 infix 4 _≤?_ _≥?_
 
 _≤?_ : Decidable _≤_
-p ≤? q = Dec.map′ *≤* drop-*≤* (↥ p ℤ.* ↧ q ℤ.≤? ↥ q ℤ.* ↧ p)
+p ≤? q = map′ *≤* drop-*≤* (↥ p ℤ.* ↧ q ℤ.≤? ↥ q ℤ.* ↧ p)
 
 _≥?_ : Decidable _≥_
 _≥?_ = flip _≤?_
@@ -652,7 +651,7 @@ toℚᵘ-isOrderMonomorphism-< = record
 infix 4 _<?_ _>?_
 
 _<?_ : Decidable _<_
-p <? q = Dec.map′ *<* drop-*<* ((↥ p ℤ.* ↧ q) ℤ.<? (↥ q ℤ.* ↧ p))
+p <? q = map′ *<* drop-*<* ((↥ p ℤ.* ↧ q) ℤ.<? (↥ q ℤ.* ↧ p))
 
 _>?_ : Decidable _>_
 _>?_ = flip _<?_
diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda
index 2ede5bb44c..873becb612 100644
--- a/src/Data/Rational/Unnormalised/Properties.agda
+++ b/src/Data/Rational/Unnormalised/Properties.agda
@@ -31,9 +31,8 @@ open import Data.Sum.Base using (_⊎_; [_,_]′; inj₁; inj₂)
 import Data.Sign as Sign
 open import Function.Base using (_on_; _$_; _∘_; flip)
 open import Level using (0ℓ)
-open import Relation.Nullary using (¬_; yes; no)
-import Relation.Nullary.Decidable as Dec
-open import Relation.Nullary.Negation using (contradiction; contraposition)
+open import Relation.Nullary.Decidable.Core using (yes; no; from-no; map′; decidable-stable)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction; contraposition)
 open import Relation.Binary.Core using (_⇒_; _Preserves_⟶_; _Preserves₂_⟶_⟶_)
 open import Relation.Binary.Bundles
   using (Setoid; DecSetoid; Preorder; TotalPreorder; Poset; TotalOrder; DecTotalOrder; StrictPartialOrder; StrictTotalOrder)
@@ -104,10 +103,10 @@ drop-*≡* (*≡* eq) = eq
 infix 4 _≃?_
 
 _≃?_ : Decidable _≃_
-p ≃? q = Dec.map′ *≡* drop-*≡* (↥ p ℤ.* ↧ q ℤ.≟ ↥ q ℤ.* ↧ p)
+p ≃? q = map′ *≡* drop-*≡* (↥ p ℤ.* ↧ q ℤ.≟ ↥ q ℤ.* ↧ p)
 
 0≠1 : 0ℚᵘ ≠ 1ℚᵘ
-0≠1 = Dec.from-no (0ℚᵘ ≃? 1ℚᵘ)
+0≠1 = from-no (0ℚᵘ ≃? 1ℚᵘ)
 
 ≃-≠-irreflexive : Irreflexive _≃_ _≠_
 ≃-≠-irreflexive x≃y x≠y = x≠y x≃y
@@ -142,7 +141,7 @@ p ≃? q = Dec.map′ *≡* drop-*≡* (↥ p ℤ.* ↧ q ℤ.≟ ↥ q ℤ.* 
   }
 
 ≠-tight : Tight _≃_ _≠_
-proj₁ (≠-tight p q) ¬p≠q = Dec.decidable-stable (p ≃? q) ¬p≠q
+proj₁ (≠-tight p q) ¬p≠q = decidable-stable (p ≃? q) ¬p≠q
 proj₂ (≠-tight p q) p≃q p≠q = p≠q p≃q
 
 ≃-setoid : Setoid 0ℓ 0ℓ
@@ -253,7 +252,7 @@ drop-*≤* (*≤* pq≤qp) = pq≤qp
 infix 4 _≤?_ _≥?_
 
 _≤?_ : Decidable _≤_
-p ≤? q = Dec.map′ *≤* drop-*≤* (↥ p ℤ.* ↧ q ℤ.≤? ↥ q ℤ.* ↧ p)
+p ≤? q = map′ *≤* drop-*≤* (↥ p ℤ.* ↧ q ℤ.≤? ↥ q ℤ.* ↧ p)
 
 _≥?_ : Decidable _≥_
 _≥?_ = flip _≤?_
@@ -456,7 +455,7 @@ drop-*<* (*<* pq<qp) = pq<qp
 infix 4 _<?_ _>?_
 
 _<?_ : Decidable _<_
-p <? q = Dec.map′ *<* drop-*<* (↥ p ℤ.* ↧ q ℤ.<? ↥ q ℤ.* ↧ p)
+p <? q = map′ *<* drop-*<* (↥ p ℤ.* ↧ q ℤ.<? ↥ q ℤ.* ↧ p)
 
 _>?_ : Decidable _>_
 _>?_ = flip _<?_
diff --git a/src/Data/Record.agda b/src/Data/Record.agda
index 6992294a5e..36019d96a9 100644
--- a/src/Data/Record.agda
+++ b/src/Data/Record.agda
@@ -18,8 +18,7 @@ open import Function.Base using (id; _∘_)
 open import Level
 open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Binary.PropositionalEquality
-open import Relation.Nullary
-open import Relation.Nullary.Decidable
+open import Relation.Nullary.Decidable.Core using (does)
 
 -- The module is parametrised by the type of labels, which should come
 -- with decidable equality.
diff --git a/src/Data/Sign/Properties.agda b/src/Data/Sign/Properties.agda
index 7ac07167e7..76afabd2de 100644
--- a/src/Data/Sign/Properties.agda
+++ b/src/Data/Sign/Properties.agda
@@ -18,7 +18,7 @@ open import Level using (0ℓ)
 open import Relation.Binary
   using (Decidable; DecidableEquality; Setoid; DecSetoid; IsDecEquivalence)
 open import Relation.Binary.PropositionalEquality
-open import Relation.Nullary.Decidable using (yes; no)
+open import Relation.Nullary.Decidable.Core using (yes; no)
 
 open import Algebra.Structures {A = Sign} _≡_
 open import Algebra.Definitions {A = Sign} _≡_
diff --git a/src/Data/String/Properties.agda b/src/Data/String/Properties.agda
index 9c5ae194e2..cbbab1e112 100644
--- a/src/Data/String/Properties.agda
+++ b/src/Data/String/Properties.agda
@@ -15,8 +15,7 @@ import Data.List.Relation.Binary.Pointwise as Pointwise
 import Data.List.Relation.Binary.Lex.Strict as StrictLex
 open import Data.String.Base
 open import Function.Base
-open import Relation.Nullary.Decidable using (yes; no)
-open import Relation.Nullary.Decidable using (map′; isYes)
+open import Relation.Nullary.Decidable.Core using (yes; no; map′; isYes)
 open import Relation.Binary.Core using (_⇒_)
 open import Relation.Binary.Bundles
   using (Setoid; DecSetoid; StrictPartialOrder; StrictTotalOrder; DecTotalOrder; DecPoset)
diff --git a/src/Data/Sum.agda b/src/Data/Sum.agda
index 99cdbd3620..3bc5a1a8b3 100644
--- a/src/Data/Sum.agda
+++ b/src/Data/Sum.agda
@@ -16,7 +16,9 @@ open import Data.Maybe.Base using (Maybe; just; nothing)
 open import Function.Base
 open import Level
 open import Relation.Nullary.Reflects using (invert)
-open import Relation.Nullary using (Dec; yes; no; _because_; ¬_)
+open import Relation.Nullary.Decidable.Core using (Dec; yes; no; _because_)
+open import Relation.Nullary.Negation.Core using (¬_)
+
 
 private
   variable
diff --git a/src/Data/Sum/Properties.agda b/src/Data/Sum/Properties.agda
index d0ba12c2fd..031fbe9bc2 100644
--- a/src/Data/Sum/Properties.agda
+++ b/src/Data/Sum/Properties.agda
@@ -14,8 +14,7 @@ open import Function.Base using (_∋_; _∘_; id)
 open import Function.Bundles using (mk↔ₛ′; _↔_)
 open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Binary.PropositionalEquality
-open import Relation.Nullary.Decidable using (yes; no)
-open import Relation.Nullary.Decidable using (map′)
+open import Relation.Nullary.Decidable.Core using (yes; no; map′)
 
 
 private
diff --git a/src/Data/Sum/Relation/Binary/LeftOrder.agda b/src/Data/Sum/Relation/Binary/LeftOrder.agda
index 397bc598dc..f554a982ce 100644
--- a/src/Data/Sum/Relation/Binary/LeftOrder.agda
+++ b/src/Data/Sum/Relation/Binary/LeftOrder.agda
@@ -15,8 +15,7 @@ open import Data.Product.Base using (_,_)
 open import Data.Empty
 open import Function.Base using (_$_; _∘_)
 open import Level
-open import Relation.Nullary
-import Relation.Nullary.Decidable as Dec
+open import Relation.Nullary.Decidable.Core using (yes; no; map′)
 open import Relation.Binary.Core using (Rel; _⇒_)
 open import Relation.Binary.Bundles
   using (Preorder; Poset; StrictPartialOrder; TotalOrder; DecTotalOrder; StrictTotalOrder)
@@ -79,10 +78,10 @@ module _ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂}
 
   ⊎-<-decidable : Decidable ∼₁ → Decidable ∼₂ →
                   Decidable (∼₁ ⊎-< ∼₂)
-  ⊎-<-decidable dec₁ dec₂ (inj₁ x) (inj₁ y) = Dec.map′ ₁∼₁ drop-inj₁ (dec₁ x y)
+  ⊎-<-decidable dec₁ dec₂ (inj₁ x) (inj₁ y) = map′ ₁∼₁ drop-inj₁ (dec₁ x y)
   ⊎-<-decidable dec₁ dec₂ (inj₁ x) (inj₂ y) = yes ₁∼₂
   ⊎-<-decidable dec₁ dec₂ (inj₂ x) (inj₁ y) = no λ()
-  ⊎-<-decidable dec₁ dec₂ (inj₂ x) (inj₂ y) = Dec.map′ ₂∼₂ drop-inj₂ (dec₂ x y)
+  ⊎-<-decidable dec₁ dec₂ (inj₂ x) (inj₂ y) = map′ ₂∼₂ drop-inj₂ (dec₂ x y)
 
 module _ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂}
          {ℓ₁ ℓ₂} {∼₁ : Rel A₁ ℓ₁} {≈₁ : Rel A₁ ℓ₂}
diff --git a/src/Data/Sum/Relation/Binary/Pointwise.agda b/src/Data/Sum/Relation/Binary/Pointwise.agda
index 943b6f5e49..5db8eefcfe 100644
--- a/src/Data/Sum/Relation/Binary/Pointwise.agda
+++ b/src/Data/Sum/Relation/Binary/Pointwise.agda
@@ -11,15 +11,15 @@ module Data.Sum.Relation.Binary.Pointwise where
 open import Data.Product.Base using (_,_)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Data.Sum.Properties
+open import Relation.Nullary.Decidable.Core using (yes; no; map′)
 open import Level using (Level; _⊔_)
 open import Function.Base using (const; _∘_; id)
 open import Function.Bundles using (Inverse; mk↔)
-open import Relation.Nullary
-import Relation.Nullary.Decidable as Dec
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 import Relation.Binary.PropositionalEquality.Properties as P
 
+
 private
   variable
     a b c d ℓ₁ ℓ₂ ℓ₃ ℓ : Level
@@ -78,11 +78,12 @@ drop-inj₂ (inj₂ x) = x
 ⊎-substitutive subst₁ subst₂ P (inj₁ x) = subst₁ (P ∘ inj₁) x
 ⊎-substitutive subst₁ subst₂ P (inj₂ x) = subst₂ (P ∘ inj₂) x
 
-⊎-decidable : Decidable R → Decidable S → Decidable (Pointwise R S)
-⊎-decidable _≟₁_ _≟₂_ (inj₁ x) (inj₁ y) = Dec.map′ inj₁ drop-inj₁ (x ≟₁ y)
+⊎-decidable : Decidable ≈₁ → Decidable ≈₂ →
+              Decidable (Pointwise ≈₁ ≈₂)
+⊎-decidable _≟₁_ _≟₂_ (inj₁ x) (inj₁ y) = map′ inj₁ drop-inj₁ (x ≟₁ y)
 ⊎-decidable _≟₁_ _≟₂_ (inj₁ x) (inj₂ y) = no λ()
 ⊎-decidable _≟₁_ _≟₂_ (inj₂ x) (inj₁ y) = no λ()
-⊎-decidable _≟₁_ _≟₂_ (inj₂ x) (inj₂ y) = Dec.map′ inj₂ drop-inj₂ (x ≟₂ y)
+⊎-decidable _≟₁_ _≟₂_ (inj₂ x) (inj₂ y) = map′ inj₂ drop-inj₂ (x ≟₂ y)
 
 ⊎-reflexive : ≈₁ ⇒ R → ≈₂ ⇒ S →
               (Pointwise ≈₁ ≈₂) ⇒ (Pointwise R S)
diff --git a/src/Data/These/Properties.agda b/src/Data/These/Properties.agda
index e7111cfce1..89ba37866f 100644
--- a/src/Data/These/Properties.agda
+++ b/src/Data/These/Properties.agda
@@ -13,7 +13,7 @@ open import Data.These.Base
 open import Function.Base using (_∘_)
 open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Binary.PropositionalEquality
-open import Relation.Nullary.Decidable using (yes; no; map′; _×-dec_)
+open import Relation.Nullary.Decidable.Core using (yes; no; map′; _×-dec_)
 
 ------------------------------------------------------------------------
 -- Equality
diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/All.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/All.agda
index 545a925f00..5ff61463fa 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/All.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/All.agda
@@ -21,7 +21,7 @@ open import Function.Nary.NonDependent using (congₙ)
 open import Level using (Level; _⊔_)
 
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
-open import Relation.Nullary.Decidable using (Dec; yes; map′; _×-dec_)
+open import Relation.Nullary.Decidable.Core using (Dec; yes; map′; _×-dec_)
 open import Relation.Unary using (Pred; Decidable; Universal; Irrelevant; _⊆_; _∪_)
 
 open StrictTotalOrder strictTotalOrder renaming (Carrier to Key)
diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
index f8c270f1a1..47e6950060 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
@@ -18,7 +18,7 @@ open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Function.Base using (_∘′_; _∘_)
 open import Level using (Level; _⊔_)
 
-open import Relation.Nullary.Decidable using (Dec; no; map′; _⊎-dec_)
+open import Relation.Nullary.Decidable.Core using (Dec; no; map′; _⊎-dec_)
 open import Relation.Unary
 
 open StrictTotalOrder strictTotalOrder renaming (Carrier to Key)
diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
index 49da62b10b..95aaf1079a 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
@@ -23,8 +23,8 @@ open import Level using (Level)
 
 open import Relation.Binary.Definitions using (_Respects_; tri<; tri≈; tri>)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_) renaming (refl to ≡-refl)
-open import Relation.Nullary using (¬_; Dec; yes; no)
-open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Nullary.Decidable.Core using (Dec; yes; no)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Unary using (Pred; _∩_)
 
 open import Data.Tree.AVL.Indexed sto as AVL
diff --git a/src/Data/Tree/AVL/Relation/Unary/Any.agda b/src/Data/Tree/AVL/Relation/Unary/Any.agda
index dfa96935ac..f57fd2e32f 100644
--- a/src/Data/Tree/AVL/Relation/Unary/Any.agda
+++ b/src/Data/Tree/AVL/Relation/Unary/Any.agda
@@ -16,7 +16,7 @@ open import Data.Product.Base as Prod using (∃)
 open import Function.Base using (_∘_; _$_)
 open import Level using (Level; _⊔_)
 
-open import Relation.Nullary.Decidable using (map′)
+open import Relation.Nullary.Decidable.Core using (map′)
 open import Relation.Unary
 
 open StrictTotalOrder strictTotalOrder renaming (Carrier to Key)
diff --git a/src/Data/Vec/Functional/Properties.agda b/src/Data/Vec/Functional/Properties.agda
index f3314754e0..5c831c1773 100644
--- a/src/Data/Vec/Functional/Properties.agda
+++ b/src/Data/Vec/Functional/Properties.agda
@@ -23,8 +23,7 @@ open import Function.Base
 open import Level using (Level)
 open import Relation.Binary.Definitions using (DecidableEquality; Decidable)
 open import Relation.Binary.PropositionalEquality
-open import Relation.Nullary.Decidable
-  using (Dec; does; yes; no; map′; _×-dec_)
+open import Relation.Nullary.Decidable.Core using (yes; no; map′; _×-dec_)
 
 import Data.Fin.Properties as Finₚ
 
diff --git a/src/Data/Vec/Membership/DecSetoid.agda b/src/Data/Vec/Membership/DecSetoid.agda
index fac9138660..a48beafa3f 100644
--- a/src/Data/Vec/Membership/DecSetoid.agda
+++ b/src/Data/Vec/Membership/DecSetoid.agda
@@ -12,7 +12,7 @@ module Data.Vec.Membership.DecSetoid {c ℓ} (DS : DecSetoid c ℓ) where
 
 open import Data.Vec.Base using (Vec)
 open import Data.Vec.Relation.Unary.Any using (any?)
-open import Relation.Nullary.Decidable using (Dec)
+open import Relation.Nullary.Decidable.Core using (Dec)
 open DecSetoid DS renaming (Carrier to A)
 
 ------------------------------------------------------------------------
diff --git a/src/Data/Vec/Relation/Binary/Lex/Core.agda b/src/Data/Vec/Relation/Binary/Lex/Core.agda
index 7b35081911..67db2840fc 100644
--- a/src/Data/Vec/Relation/Binary/Lex/Core.agda
+++ b/src/Data/Vec/Relation/Binary/Lex/Core.agda
@@ -26,7 +26,7 @@ open import Relation.Binary.PropositionalEquality.Core as P
   using (_≡_; refl; cong)
 import Relation.Nullary as Nullary
 open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _×-dec_; _⊎-dec_)
-open import Relation.Nullary.Negation
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 
 private
   variable
diff --git a/src/Data/Vec/Relation/Binary/Pointwise/Extensional.agda b/src/Data/Vec/Relation/Binary/Pointwise/Extensional.agda
index 5dcaa6b900..790353ad28 100644
--- a/src/Data/Vec/Relation/Binary/Pointwise/Extensional.agda
+++ b/src/Data/Vec/Relation/Binary/Pointwise/Extensional.agda
@@ -25,8 +25,8 @@ open import Relation.Binary.Definitions using (Reflexive; Sym; Trans; Decidable)
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 open import Relation.Binary.Construct.Closure.Transitive as Plus
   hiding (equivalent; map)
-open import Relation.Nullary
-import Relation.Nullary.Decidable as Dec
+open import Relation.Nullary.Decidable.Core using (map′)
+open import Relation.Nullary.Negation.Core using (¬_)
 
 private
   variable
@@ -110,8 +110,7 @@ trans trns xs∼ys ys∼zs = ext λ i →
 
 decidable : ∀ {_∼_ : REL A B ℓ} →
             Decidable _∼_ → ∀ {n} → Decidable (Pointwise _∼_ {n = n})
-decidable dec xs ys = Dec.map
-  (Setoid.sym (⇔-setoid _) equivalent)
+decidable dec xs ys = map′ inductive⇒extensional extensional⇒inductive
   (Inductive.decidable dec xs ys)
 
 isEquivalence : ∀ {_∼_ : Rel A ℓ} {n} →
diff --git a/src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda b/src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda
index c6835b73e1..918e3fd8ab 100644
--- a/src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda
+++ b/src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda
@@ -23,7 +23,7 @@ open import Relation.Binary.Structures
 open import Relation.Binary.Definitions
   using (Trans; Decidable; Reflexive; Sym)
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
-open import Relation.Nullary.Decidable using (yes; no; _×-dec_; map′)
+open import Relation.Nullary.Decidable.Core using (yes; no; _×-dec_; map′)
 open import Relation.Unary using (Pred)
 
 private
diff --git a/src/Data/Vec/Relation/Unary/All.agda b/src/Data/Vec/Relation/Unary/All.agda
index e8d24fbd65..9292e533eb 100644
--- a/src/Data/Vec/Relation/Unary/All.agda
+++ b/src/Data/Vec/Relation/Unary/All.agda
@@ -17,7 +17,7 @@ open import Data.Vec.Membership.Propositional renaming (_∈_ to _∈ₚ_)
 import Data.Vec.Membership.Setoid as SetoidMembership
 open import Function.Base using (_∘_)
 open import Level using (Level; _⊔_)
-open import Relation.Nullary.Decidable as Dec using (_×-dec_; yes; no)
+open import Relation.Nullary.Decidable.Core using (_×-dec_; yes; no; map′)
 open import Relation.Unary hiding (_∈_)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Definitions using (_Respects_)
@@ -108,7 +108,7 @@ module _(S : Setoid a ℓ) {P : Pred (Setoid.Carrier S) p} where
 
 all? : ∀ {n} → Decidable P → Decidable (All P {n})
 all? P? []       = yes []
-all? P? (x ∷ xs) = Dec.map′ (uncurry _∷_) uncons (P? x ×-dec all? P? xs)
+all? P? (x ∷ xs) = map′ (uncurry _∷_) uncons (P? x ×-dec all? P? xs)
 
 universal : Universal P → ∀ {n} → Universal (All P {n})
 universal u []       = []
diff --git a/src/Data/Vec/Relation/Unary/AllPairs.agda b/src/Data/Vec/Relation/Unary/AllPairs.agda
index a702a1dbf9..8c85f24151 100644
--- a/src/Data/Vec/Relation/Unary/AllPairs.agda
+++ b/src/Data/Vec/Relation/Unary/AllPairs.agda
@@ -21,7 +21,7 @@ open import Relation.Binary.Definitions as B
 open import Relation.Binary.Construct.Intersection renaming (_∩_ to _∩ᵇ_)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Unary as U renaming (_∩_ to _∩ᵘ_) hiding (_⇒_)
-open import Relation.Nullary.Decidable as Dec using (yes; no; _×-dec_)
+open import Relation.Nullary.Decidable.Core using (yes; no; _×-dec_; map′)
 
 ------------------------------------------------------------------------
 -- Definition
@@ -71,7 +71,7 @@ module _ {s} {S : Rel A s} where
 allPairs? : ∀ {n} → B.Decidable R → U.Decidable (AllPairs R {n})
 allPairs? R? []       = yes []
 allPairs? R? (x ∷ xs) =
-  Dec.map′ (uncurry _∷_) uncons (All.all? (R? x) xs ×-dec allPairs? R? xs)
+  map′ (uncurry _∷_) uncons (All.all? (R? x) xs ×-dec allPairs? R? xs)
 
 irrelevant : ∀ {n} → B.Irrelevant R → U.Irrelevant (AllPairs R {n})
 irrelevant irr []           []           = refl
diff --git a/src/Data/Vec/Relation/Unary/Any.agda b/src/Data/Vec/Relation/Unary/Any.agda
index de901fe571..29ac2876e0 100644
--- a/src/Data/Vec/Relation/Unary/Any.agda
+++ b/src/Data/Vec/Relation/Unary/Any.agda
@@ -15,8 +15,8 @@ open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Data.Vec.Base as Vec using (Vec; []; [_]; _∷_)
 open import Data.Product.Base as Prod using (∃; _,_)
 open import Level using (Level; _⊔_)
-open import Relation.Nullary.Negation using (¬_; contradiction)
-open import Relation.Nullary.Decidable as Dec using (yes; no; _⊎-dec_)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
+open import Relation.Nullary.Decidable.Core using (yes; no; _⊎-dec_; map′)
 open import Relation.Unary
 
 private
@@ -76,7 +76,7 @@ satisfied (there pxs) = satisfied pxs
 
 any? : Decidable P → ∀ {n} → Decidable (Any P {n})
 any? P? []       = no λ()
-any? P? (x ∷ xs) = Dec.map′ fromSum toSum (P? x ⊎-dec any? P? xs)
+any? P? (x ∷ xs) = map′ fromSum toSum (P? x ⊎-dec any? P? xs)
 
 satisfiable : Satisfiable P → ∀ {n} → Satisfiable (Any P {suc n})
 satisfiable (x , p) {zero}  = x ∷ [] , here p
diff --git a/src/Data/Vec/Relation/Unary/Linked.agda b/src/Data/Vec/Relation/Unary/Linked.agda
index 368c22ddc1..1184786ec8 100644
--- a/src/Data/Vec/Relation/Unary/Linked.agda
+++ b/src/Data/Vec/Relation/Unary/Linked.agda
@@ -19,7 +19,7 @@ open import Relation.Binary.Definitions as B
 open import Relation.Binary.Construct.Intersection renaming (_∩_ to _∩ᵇ_)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Unary as U renaming (_∩_ to _∩ᵘ_) hiding (_⇒_)
-open import Relation.Nullary.Decidable as Dec using (yes; no; _×-dec_; map′)
+open import Relation.Nullary.Decidable.Core using (yes; no; _×-dec_; map′)
 
 private
   variable
diff --git a/src/Data/Vec/Relation/Unary/Linked/Properties.agda b/src/Data/Vec/Relation/Unary/Linked/Properties.agda
index c32e4c8df6..eb2010a706 100644
--- a/src/Data/Vec/Relation/Unary/Linked/Properties.agda
+++ b/src/Data/Vec/Relation/Unary/Linked/Properties.agda
@@ -24,7 +24,7 @@ open import Relation.Binary.Definitions using (Transitive)
 open import Relation.Binary.Bundles using (DecSetoid)
 open import Relation.Binary.PropositionalEquality.Core using (_≢_)
 open import Relation.Unary using (Pred; Decidable)
-open import Relation.Nullary.Decidable using (yes; no; does)
+
 
 private
   variable
diff --git a/src/Data/Vec/Relation/Unary/Unique/Propositional/Properties.agda b/src/Data/Vec/Relation/Unary/Unique/Propositional/Properties.agda
index 8e1fe54b4f..6ba412c596 100644
--- a/src/Data/Vec/Relation/Unary/Unique/Propositional/Properties.agda
+++ b/src/Data/Vec/Relation/Unary/Unique/Propositional/Properties.agda
@@ -25,7 +25,7 @@ open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.PropositionalEquality
   using (refl; _≡_; _≢_; sym; setoid)
 open import Relation.Unary using (Pred; Decidable)
-open import Relation.Nullary.Negation using (¬_)
+open import Relation.Nullary.Negation.Core using (¬_)
 
 private
   variable
diff --git a/src/Data/Word/Properties.agda b/src/Data/Word/Properties.agda
index 3f9ad94ef1..f96d2bc32d 100644
--- a/src/Data/Word/Properties.agda
+++ b/src/Data/Word/Properties.agda
@@ -13,7 +13,7 @@ open import Data.Bool.Base using (Bool)
 open import Data.Word.Base
 import Data.Nat.Properties as ℕₚ
 open import Function.Base
-open import Relation.Nullary.Decidable using (map′; ⌊_⌋)
+open import Relation.Nullary.Decidable.Core using (map′; ⌊_⌋)
 open import Relation.Binary
   using ( _⇒_; Reflexive; Symmetric; Transitive; Substitutive
         ; Decidable; DecidableEquality; IsEquivalence; IsDecEquivalence
diff --git a/src/Effect/Monad/Partiality.agda b/src/Effect/Monad/Partiality.agda
index 5fb6ec3455..1714f2e42a 100644
--- a/src/Effect/Monad/Partiality.agda
+++ b/src/Effect/Monad/Partiality.agda
@@ -29,8 +29,7 @@ open import Relation.Binary.Bundles
 import Relation.Binary.Properties.Setoid as SetoidProperties
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 import Relation.Binary.PropositionalEquality.Properties as P
-open import Relation.Nullary
-open import Relation.Nullary.Decidable hiding (map)
+open import Relation.Nullary.Decidable.Core
 open import Relation.Nullary.Negation
 
 private
diff --git a/src/Function/Related/TypeIsomorphisms.agda b/src/Function/Related/TypeIsomorphisms.agda
index 830bb6f8bb..7b810aba04 100644
--- a/src/Function/Related/TypeIsomorphisms.agda
+++ b/src/Function/Related/TypeIsomorphisms.agda
@@ -13,8 +13,7 @@ open import Algebra
 open import Algebra.Structures.Biased using (isCommutativeSemiringˡ)
 open import Axiom.Extensionality.Propositional using (Extensionality)
 open import Data.Bool.Base using (true; false)
-open import Data.Empty using (⊥-elim)
-open import Data.Empty.Polymorphic using (⊥) renaming (⊥-elim to ⊥ₚ-elim)
+open import Data.Empty.Polymorphic using (⊥; ⊥-elim)
 open import Data.Product.Base as Prod
   using (_×_; Σ; curry; uncurry; _,_; -,_; <_,_>; proj₁; proj₂; ∃₂; ∃)
 open import Data.Product.Function.NonDependent.Propositional
@@ -27,12 +26,13 @@ open import Function.Base
 open import Function.Bundles
 open import Function.Related.Propositional
 import Function.Construct.Identity as Identity
-open import Relation.Binary hiding (_⇔_)
+open import Relation.Binary hiding (_⇔_; Irrelevant)
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
+open import Relation.Nullary using (Irrelevant)
+open import Relation.Nullary.Decidable.Core using (Dec; _because_; True)
+open import Relation.Nullary.Decidable using (True-↔)
 open import Relation.Nullary.Reflects using (invert)
-open import Relation.Nullary using (Dec; ¬_; _because_; ofⁿ)
-import Relation.Nullary.Indexed as I
-open import Relation.Nullary.Decidable using (True)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 
 private
   variable
@@ -66,10 +66,10 @@ private
 -- × has ⊥ has its zero
 
 ×-zeroˡ : ∀ ℓ → LeftZero {ℓ = ℓ} _↔_ ⊥ _×_
-×-zeroˡ ℓ A = mk↔ₛ′ proj₁ < id , ⊥ₚ-elim > (λ _ → P.refl) (λ { () })
+×-zeroˡ ℓ A = mk↔ₛ′ proj₁ < id , ⊥-elim > (λ _ → P.refl) (λ { () })
 
 ×-zeroʳ : ∀ ℓ → RightZero {ℓ = ℓ} _↔_ ⊥ _×_
-×-zeroʳ ℓ A = mk↔ₛ′ proj₂ < ⊥ₚ-elim , id > (λ _ → P.refl) (λ { () })
+×-zeroʳ ℓ A = mk↔ₛ′ proj₂ < ⊥-elim , id > (λ _ → P.refl) (λ { () })
 
 ×-zero : ∀ ℓ → Zero _↔_ ⊥ _×_
 ×-zero ℓ  = ×-zeroˡ ℓ , ×-zeroʳ ℓ
@@ -325,9 +325,57 @@ Related-cong {A = A} {B = B} {C = C} {D = D} A≈B C≈D = mk⇔
 ------------------------------------------------------------------------
 -- A lemma relating True dec and P, where dec : Dec P
 
-True↔ : ∀ {p} {P : Set p}
-        (dec : Dec P) → ((p₁ p₂ : P) → p₁ ≡ p₂) → True dec ↔ P
-True↔ ( true because  [p]) irr =
-  mk↔ₛ′ (λ _ → invert [p]) (λ _ → _) (irr _) (λ _ → P.refl)
-True↔ (false because ofⁿ ¬p) _ =
-  mk↔ₛ′ (λ()) (invert (ofⁿ ¬p)) (⊥-elim ∘ ¬p) (λ ())
+True↔ : (dec : Dec A) → Irrelevant A → True dec ↔ A
+True↔ = True-↔
+
+------------------------------------------------------------------------
+-- Equality between pairs can be expressed as a pair of equalities
+
+module _ {a b} {A : Set a} {B : A → Set b} {p₁ p₂ : Σ A B} where
+  Σ-≡,≡→≡ : Σ (proj₁ p₁ ≡ proj₁ p₂)
+              (λ p → P.subst B p (proj₂ p₁) ≡ proj₂ p₂) →
+            p₁ ≡ p₂
+  Σ-≡,≡→≡ (P.refl , P.refl) = P.refl
+
+  Σ-≡,≡←≡ : p₁ ≡ p₂ →
+            Σ (proj₁ p₁ ≡ proj₁ p₂)
+              (λ p → P.subst B p (proj₂ p₁) ≡ proj₂ p₂)
+  Σ-≡,≡←≡ P.refl = P.refl , P.refl
+
+  private
+
+    left-inverse-of : (p : Σ (proj₁ p₁ ≡ proj₁ p₂)
+                             (λ x → P.subst B x (proj₂ p₁) ≡ proj₂ p₂)) →
+                      Σ-≡,≡←≡ (Σ-≡,≡→≡ p) ≡ p
+    left-inverse-of (P.refl , P.refl) = P.refl
+
+    right-inverse-of : (p : p₁ ≡ p₂) → Σ-≡,≡→≡ (Σ-≡,≡←≡ p) ≡ p
+    right-inverse-of P.refl = P.refl
+
+  Σ-≡,≡↔≡ : (∃ λ (p : proj₁ p₁ ≡ proj₁ p₂) →
+               P.subst B p (proj₂ p₁) ≡ proj₂ p₂) ↔
+            p₁ ≡ p₂
+  Σ-≡,≡↔≡ = mk↔ₛ′ Σ-≡,≡→≡ Σ-≡,≡←≡ right-inverse-of left-inverse-of
+
+module _ {a b} {A : Set a} {B : Set b} {p₁ p₂ : A × B} where
+  ×-≡,≡→≡ : (proj₁ p₁ ≡ proj₁ p₂) × (proj₂ p₁ ≡ proj₂ p₂) → p₁ ≡ p₂
+  ×-≡,≡→≡ (P.refl , P.refl) = P.refl
+
+  ×-≡,≡←≡ : p₁ ≡ p₂ →
+            (proj₁ p₁ ≡ proj₁ p₂) × (proj₂ p₁ ≡ proj₂ p₂)
+  ×-≡,≡←≡ P.refl = P.refl , P.refl
+
+  private
+    left-inverse-of : (p : (proj₁ p₁ ≡ proj₁ p₂) × (proj₂ p₁ ≡ proj₂ p₂)) →
+                      ×-≡,≡←≡ (×-≡,≡→≡ p) ≡ p
+    left-inverse-of (P.refl , P.refl) = P.refl
+
+    right-inverse-of : (p : p₁ ≡ p₂) → ×-≡,≡→≡ (×-≡,≡←≡ p) ≡ p
+    right-inverse-of P.refl = P.refl
+
+  ×-≡,≡↔≡ : (proj₁ p₁ ≡ proj₁ p₂ × proj₂ p₁ ≡ proj₂ p₂) ↔ p₁ ≡ p₂
+  ×-≡,≡↔≡ = mk↔ₛ′ ×-≡,≡→≡ ×-≡,≡←≡ right-inverse-of left-inverse-of
+
+×-≡×≡↔≡,≡ : ∀ {a b} {A : Set a} {B : Set b} {x y} (p : A × B) →
+            (x ≡ proj₁ p × y ≡ proj₂ p) ↔ (x , y) ≡ p
+×-≡×≡↔≡,≡ _ = ×-≡,≡↔≡
diff --git a/src/Reflection/AST/Argument/Quantity.agda b/src/Reflection/AST/Argument/Quantity.agda
index ff0a0d3c65..9eee622b67 100644
--- a/src/Reflection/AST/Argument/Quantity.agda
+++ b/src/Reflection/AST/Argument/Quantity.agda
@@ -8,7 +8,7 @@
 
 module Reflection.AST.Argument.Quantity where
 
-open import Relation.Nullary.Decidable.Core           using (yes; no)
+open import Relation.Nullary.Decidable.Core            using (yes; no)
 open import Relation.Binary.Definitions                using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (refl)
 
diff --git a/src/Reflection/AST/Term.agda b/src/Reflection/AST/Term.agda
index cdcefb55fc..db03e3fbc6 100644
--- a/src/Reflection/AST/Term.agda
+++ b/src/Reflection/AST/Term.agda
@@ -17,7 +17,7 @@ open import Data.Product.Properties                    using (,-injective)
 open import Data.Maybe.Base                            using (Maybe; just; nothing)
 open import Data.String.Base                           using (String)
 open import Data.String.Properties as String           hiding (_≟_)
-open import Relation.Nullary.Decidable                 using (map′; _×-dec_; yes; no)
+open import Relation.Nullary.Decidable.Core            using (map′; _×-dec_; yes; no)
 open import Relation.Binary.Definitions                using (Decidable; DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; cong₂)
 
diff --git a/src/Relation/Binary/Construct/Add/Infimum/NonStrict.agda b/src/Relation/Binary/Construct/Add/Infimum/NonStrict.agda
index 5d5cb2a214..cccb96876c 100644
--- a/src/Relation/Binary/Construct/Add/Infimum/NonStrict.agda
+++ b/src/Relation/Binary/Construct/Add/Infimum/NonStrict.agda
@@ -24,9 +24,8 @@ open import Relation.Binary.PropositionalEquality.Core as P
   using (_≡_; refl)
 import Relation.Binary.PropositionalEquality.Properties as P
 import Relation.Binary.Construct.Add.Infimum.Equality as Equality
-open import Relation.Nullary hiding (Irrelevant)
 open import Relation.Nullary.Construct.Add.Infimum
-import Relation.Nullary.Decidable as Dec
+open import Relation.Nullary.Decidable.Core using (yes; no; map′)
 
 ------------------------------------------------------------------------
 -- Definition
@@ -52,7 +51,7 @@ data _≤₋_ : Rel (A ₋) (a ⊔ ℓ) where
 ≤₋-dec : Decidable _≤_ → Decidable _≤₋_
 ≤₋-dec _≤?_ ⊥₋    l     = yes (⊥₋≤ l)
 ≤₋-dec _≤?_ [ k ] ⊥₋    = no (λ ())
-≤₋-dec _≤?_ [ k ] [ l ] = Dec.map′ [_] [≤]-injective (k ≤? l)
+≤₋-dec _≤?_ [ k ] [ l ] = map′ [_] [≤]-injective (k ≤? l)
 
 ≤₋-total : Total _≤_ → Total _≤₋_
 ≤₋-total ≤-total ⊥₋    l     = inj₁ (⊥₋≤ l)
diff --git a/src/Relation/Binary/Construct/Add/Infimum/Strict.agda b/src/Relation/Binary/Construct/Add/Infimum/Strict.agda
index ae96849340..3f820e6237 100644
--- a/src/Relation/Binary/Construct/Add/Infimum/Strict.agda
+++ b/src/Relation/Binary/Construct/Add/Infimum/Strict.agda
@@ -26,9 +26,8 @@ open import Relation.Binary.PropositionalEquality.Core as P
 import Relation.Binary.PropositionalEquality.Properties as P
 import Relation.Binary.Construct.Add.Infimum.Equality as Equality
 import Relation.Binary.Construct.Add.Infimum.NonStrict as NonStrict
-open import Relation.Nullary hiding (Irrelevant)
 open import Relation.Nullary.Construct.Add.Infimum
-import Relation.Nullary.Decidable as Dec
+open import Relation.Nullary.Decidable.Core
 
 ------------------------------------------------------------------------
 -- Definition
@@ -56,7 +55,7 @@ data _<₋_ : Rel (A ₋) (a ⊔ ℓ) where
 <₋-dec _<?_ ⊥₋    ⊥₋    = no (λ ())
 <₋-dec _<?_ ⊥₋    [ l ] = yes ⊥₋<[ l ]
 <₋-dec _<?_ [ k ] ⊥₋    = no (λ ())
-<₋-dec _<?_ [ k ] [ l ] = Dec.map′ [_] [<]-injective (k <? l)
+<₋-dec _<?_ [ k ] [ l ] = map′ [_] [<]-injective (k <? l)
 
 <₋-irrelevant : Irrelevant _<_ → Irrelevant _<₋_
 <₋-irrelevant <-irr ⊥₋<[ l ] ⊥₋<[ l ] = P.refl
diff --git a/src/Relation/Binary/Construct/Add/Point/Equality.agda b/src/Relation/Binary/Construct/Add/Point/Equality.agda
index 704d963123..6c247eae1a 100644
--- a/src/Relation/Binary/Construct/Add/Point/Equality.agda
+++ b/src/Relation/Binary/Construct/Add/Point/Equality.agda
@@ -21,9 +21,8 @@ module Relation.Binary.Construct.Add.Point.Equality
 open import Level using (_⊔_)
 open import Function.Base
 import Relation.Binary.PropositionalEquality.Core as P
-open import Relation.Nullary hiding (Irrelevant)
 open import Relation.Nullary.Construct.Add.Point
-import Relation.Nullary.Decidable as Dec
+open import Relation.Nullary.Decidable.Core using (yes; no; map′)
 
 ------------------------------------------------------------------------
 -- Definition
@@ -56,7 +55,7 @@ data _≈∙_ : Rel (Pointed A) (a ⊔ ℓ) where
 ≈∙-dec _≟_ ∙     ∙     = yes ∙≈∙
 ≈∙-dec _≟_ ∙     [ l ] = no (λ ())
 ≈∙-dec _≟_ [ k ] ∙     = no (λ ())
-≈∙-dec _≟_ [ k ] [ l ] = Dec.map′ [_] [≈]-injective (k ≟ l)
+≈∙-dec _≟_ [ k ] [ l ] = map′ [_] [≈]-injective (k ≟ l)
 
 ≈∙-irrelevant : Irrelevant _≈_ → Irrelevant _≈∙_
 ≈∙-irrelevant ≈-irr ∙≈∙   ∙≈∙   = P.refl
diff --git a/src/Relation/Binary/Construct/Add/Supremum/NonStrict.agda b/src/Relation/Binary/Construct/Add/Supremum/NonStrict.agda
index b550dd4924..7f6c94f6bf 100644
--- a/src/Relation/Binary/Construct/Add/Supremum/NonStrict.agda
+++ b/src/Relation/Binary/Construct/Add/Supremum/NonStrict.agda
@@ -20,8 +20,7 @@ module Relation.Binary.Construct.Add.Supremum.NonStrict
 
 open import Level using (_⊔_)
 open import Data.Sum.Base as Sum
-open import Relation.Nullary hiding (Irrelevant)
-import Relation.Nullary.Decidable as Dec
+open import Relation.Nullary.Decidable.Core using (yes; no; map′)
 open import Relation.Binary.PropositionalEquality.Core as P
   using (_≡_; refl)
 import Relation.Binary.PropositionalEquality.Properties as P
@@ -53,7 +52,7 @@ data _≤⁺_ : Rel (A ⁺) (a ⊔ ℓ) where
 ≤⁺-dec : Decidable _≤_ → Decidable _≤⁺_
 ≤⁺-dec _≤?_ k     ⊤⁺    = yes (k ≤⊤⁺)
 ≤⁺-dec _≤?_ ⊤⁺    [ l ] = no (λ ())
-≤⁺-dec _≤?_ [ k ] [ l ] = Dec.map′ [_] [≤]-injective (k ≤? l)
+≤⁺-dec _≤?_ [ k ] [ l ] = map′ [_] [≤]-injective (k ≤? l)
 
 ≤⁺-total : Total _≤_ → Total _≤⁺_
 ≤⁺-total ≤-total k     ⊤⁺    = inj₁ (k ≤⊤⁺)
diff --git a/src/Relation/Binary/Construct/Add/Supremum/Strict.agda b/src/Relation/Binary/Construct/Add/Supremum/Strict.agda
index d927cf45c4..2ffd861912 100644
--- a/src/Relation/Binary/Construct/Add/Supremum/Strict.agda
+++ b/src/Relation/Binary/Construct/Add/Supremum/Strict.agda
@@ -21,8 +21,7 @@ module Relation.Binary.Construct.Add.Supremum.Strict
 open import Level using (_⊔_)
 open import Data.Product.Base using (_,_; map)
 open import Function.Base
-open import Relation.Nullary hiding (Irrelevant)
-import Relation.Nullary.Decidable as Dec
+open import Relation.Nullary.Decidable.Core using (yes; no; map′)
 open import Relation.Binary.PropositionalEquality.Core as P
   using (_≡_; refl)
 import Relation.Binary.PropositionalEquality.Properties as P
@@ -53,7 +52,7 @@ data _<⁺_ : Rel (A ⁺) (a ⊔ r) where
 <⁺-trans <-trans [ p ] [ k ]<⊤⁺ = [ _ ]<⊤⁺
 
 <⁺-dec : Decidable _<_ → Decidable _<⁺_
-<⁺-dec _<?_ [ k ] [ l ] = Dec.map′ [_] [<]-injective (k <? l)
+<⁺-dec _<?_ [ k ] [ l ] = map′ [_] [<]-injective (k <? l)
 <⁺-dec _<?_ [ k ] ⊤⁺    = yes [ k ]<⊤⁺
 <⁺-dec _<?_ ⊤⁺    [ l ] = no (λ ())
 <⁺-dec _<?_ ⊤⁺    ⊤⁺    = no (λ ())
diff --git a/src/Relation/Binary/Construct/Closure/Reflexive/Properties.agda b/src/Relation/Binary/Construct/Closure/Reflexive/Properties.agda
index 29defea059..8db15c95b8 100644
--- a/src/Relation/Binary/Construct/Closure/Reflexive/Properties.agda
+++ b/src/Relation/Binary/Construct/Closure/Reflexive/Properties.agda
@@ -21,8 +21,8 @@ open import Relation.Binary.Definitions
 open import Relation.Binary.Construct.Closure.Reflexive
 open import Relation.Binary.PropositionalEquality.Core as PropEq using (_≡_; refl)
 import Relation.Binary.PropositionalEquality.Properties as PropEq
-open import Relation.Nullary
-import Relation.Nullary.Decidable as Dec
+open import Relation.Nullary.Decidable.Core using (yes; no; map′; _⊎-dec_)
+open import Relation.Nullary.Negation.Core using (contradiction)
 open import Relation.Unary using (Pred)
 
 private
@@ -79,7 +79,7 @@ module _ {_~_ : Rel A ℓ} where
   ... | tri> _ _    c = inj₂ [ c ]
 
   dec : Decidable {A = A} _≡_ → Decidable _~_ → Decidable _~ᵒ_
-  dec ≡-dec ~-dec a b = Dec.map ⊎⇔Refl (≡-dec a b ⊎-dec ~-dec a b)
+  dec ≡-dec ~-dec a b = map′ fromSum toSum (≡-dec a b ⊎-dec ~-dec a b)
 
   decidable : Trichotomous _≡_ _~_ → Decidable _~ᵒ_
   decidable ~-tri a b with ~-tri a b
diff --git a/src/Relation/Binary/Construct/Intersection.agda b/src/Relation/Binary/Construct/Intersection.agda
index 0d26d675e6..4b5459f974 100644
--- a/src/Relation/Binary/Construct/Intersection.agda
+++ b/src/Relation/Binary/Construct/Intersection.agda
@@ -12,12 +12,12 @@ open import Data.Product.Base
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
 open import Function.Base using (_∘_)
 open import Level using (Level; _⊔_)
+open import Relation.Nullary.Decidable.Core using (yes; no; _×-dec_)
 open import Relation.Binary.Core using (Rel; REL; _⇒_)
 open import Relation.Binary.Structures
   using (IsEquivalence; IsDecEquivalence; IsPreorder; IsPartialOrder; IsStrictPartialOrder)
 open import Relation.Binary.Definitions
   using (Reflexive; Symmetric; Transitive; Antisymmetric; Decidable; _Respects_; _Respectsˡ_; _Respectsʳ_; _Respects₂_; Minimum; Maximum; Irreflexive)
-open import Relation.Nullary.Decidable using (yes; no; _×-dec_)
 
 private
   variable
diff --git a/src/Relation/Binary/Construct/NonStrictToStrict.agda b/src/Relation/Binary/Construct/NonStrictToStrict.agda
index c2eb114004..023018fdcb 100644
--- a/src/Relation/Binary/Construct/NonStrictToStrict.agda
+++ b/src/Relation/Binary/Construct/NonStrictToStrict.agda
@@ -18,9 +18,8 @@ module Relation.Binary.Construct.NonStrictToStrict
 open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Function.Base using (_∘_; flip)
-open import Relation.Nullary using (¬_; yes; no)
-open import Relation.Nullary.Negation using (contradiction)
-open import Relation.Nullary.Decidable using (¬?; _×-dec_)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
+open import Relation.Nullary.Decidable.Core using (yes; no; ¬?; _×-dec_)
 
 private
   _≉_ : Rel A ℓ₁
diff --git a/src/Relation/Binary/Construct/StrictToNonStrict.agda b/src/Relation/Binary/Construct/StrictToNonStrict.agda
index d17b6017fc..c5526a3362 100644
--- a/src/Relation/Binary/Construct/StrictToNonStrict.agda
+++ b/src/Relation/Binary/Construct/StrictToNonStrict.agda
@@ -26,7 +26,7 @@ open import Data.Sum.Base
 open import Data.Empty
 open import Function.Base
 open import Relation.Binary.Consequences
-open import Relation.Nullary.Decidable using (_⊎-dec_; yes; no)
+open import Relation.Nullary.Decidable.Core using (_⊎-dec_; yes; no)
 
 ------------------------------------------------------------------------
 -- Conversion
diff --git a/src/Relation/Binary/Construct/Union.agda b/src/Relation/Binary/Construct/Union.agda
index 45f72c8190..045d955f1f 100644
--- a/src/Relation/Binary/Construct/Union.agda
+++ b/src/Relation/Binary/Construct/Union.agda
@@ -12,10 +12,10 @@ open import Data.Product.Base
 open import Data.Sum.Base as Sum
 open import Function.Base using (_∘_)
 open import Level using (Level; _⊔_)
+open import Relation.Nullary.Decidable.Core using (yes; no; _⊎-dec_)
 open import Relation.Binary.Core using (REL; Rel; _⇒_)
 open import Relation.Binary.Definitions
   using (Reflexive; Total; Minimum; Maximum; Symmetric; Irreflexive; Decidable; _Respects_; _Respectsˡ_; _Respectsʳ_; _Respects₂_)
-open import Relation.Nullary.Decidable using (yes; no; _⊎-dec_)
 
 private
   variable
diff --git a/src/Relation/Binary/Morphism/RelMonomorphism.agda b/src/Relation/Binary/Morphism/RelMonomorphism.agda
index 73a873fae5..f4dbdb9909 100644
--- a/src/Relation/Binary/Morphism/RelMonomorphism.agda
+++ b/src/Relation/Binary/Morphism/RelMonomorphism.agda
@@ -23,8 +23,7 @@ module Relation.Binary.Morphism.RelMonomorphism
   where
 
 open import Data.Sum.Base as Sum
-open import Relation.Nullary.Decidable using (yes; no)
-open import Relation.Nullary.Decidable
+open import Relation.Nullary.Decidable.Core using (yes; no; map′)
 
 open IsRelMonomorphism isMonomorphism
 
diff --git a/src/Relation/Binary/Reasoning/Base/Apartness.agda b/src/Relation/Binary/Reasoning/Base/Apartness.agda
index 6e0e239a02..9714ad95c0 100644
--- a/src/Relation/Binary/Reasoning/Base/Apartness.agda
+++ b/src/Relation/Binary/Reasoning/Base/Apartness.agda
@@ -21,8 +21,7 @@ module Relation.Binary.Reasoning.Base.Apartness {a ℓ₁ ℓ₂} {A : Set a}
 open import Level using (Level; _⊔_)
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; refl; sym)
-open import Relation.Nullary.Decidable using (Dec; yes; no)
-open import Relation.Nullary.Decidable using (True; toWitness)
+open import Relation.Nullary.Decidable.Core using (Dec; yes; no; True; toWitness)
 
 open IsEquivalence ≈-equiv
   renaming
diff --git a/src/Relation/Binary/Reasoning/Base/Partial.agda b/src/Relation/Binary/Reasoning/Base/Partial.agda
index e53f7e4efe..72938d9d64 100644
--- a/src/Relation/Binary/Reasoning/Base/Partial.agda
+++ b/src/Relation/Binary/Reasoning/Base/Partial.agda
@@ -11,8 +11,7 @@ open import Relation.Binary.Definitions
 open import Level using (_⊔_)
 open import Relation.Binary.PropositionalEquality.Core as P
   using (_≡_)
-open import Relation.Nullary.Decidable using (Dec; yes; no)
-open import Relation.Nullary.Decidable using (True)
+open import Relation.Nullary.Decidable.Core using (Dec; yes; no; True)
 
 module Relation.Binary.Reasoning.Base.Partial
   {a ℓ} {A : Set a} (_∼_ : Rel A ℓ) (trans : Transitive _∼_)
diff --git a/src/Relation/Binary/Reasoning/Base/Single.agda b/src/Relation/Binary/Reasoning/Base/Single.agda
index 43b553c7d1..a164a5a0de 100644
--- a/src/Relation/Binary/Reasoning/Base/Single.agda
+++ b/src/Relation/Binary/Reasoning/Base/Single.agda
@@ -16,7 +16,7 @@ module Relation.Binary.Reasoning.Base.Single
 
 -- TODO: the following part is copied from Relation.Binary.Reasoning.Base.Partial
 -- in order to avoid larger refactors. We will refactor this part later
--- so taht we use the same framework as Relation.Binary.Reasoning.Base.Partial.
+-- so that we use the same framework as Relation.Binary.Reasoning.Base.Partial.
 
 open import Level using (_⊔_)
 open import Relation.Binary.PropositionalEquality.Core as P
diff --git a/src/Relation/Nary.agda b/src/Relation/Nary.agda
index 6610b16439..c97df4062c 100644
--- a/src/Relation/Nary.agda
+++ b/src/Relation/Nary.agda
@@ -24,8 +24,8 @@ open import Data.Product.Nary.NonDependent
 open import Data.Sum.Base using (_⊎_)
 open import Function.Base using (_$_; _∘′_)
 open import Function.Nary.NonDependent
-open import Relation.Nullary.Negation using (¬_)
-open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _because_; _×-dec_)
+open import Relation.Nullary.Negation.Core using (¬_)
+open import Relation.Nullary.Decidable.Core hiding (⌊_⌋; toWitness; fromWitness)
 import Relation.Unary as Unary
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong; subst)
 
@@ -85,7 +85,7 @@ infix 5 ∃⟨_⟩ Π[_] ∀[_]
          ∀ {l r} → Arrows n (Dec <$> Equalₙ n l r) (Dec (uncurryₙ n con l ≡ uncurryₙ n con r))
 ≟-mapₙ n con con-inj =
   curryₙ n λ a?s → let as? = Product-dec n a?s in
-  Dec.map′ (cong (uncurryₙ n con) ∘′ fromEqualₙ n) con-inj as?
+  map′ (cong (uncurryₙ n con) ∘′ fromEqualₙ n) con-inj as?
 
 ------------------------------------------------------------------------
 -- Substitution
@@ -187,7 +187,7 @@ Decidable R = Π[ mapₙ _ Dec R ]
 -- erasure
 
 ⌊_⌋ : ∀ {n ls r} {as : Sets n ls} {R : as ⇉ Set r} → Decidable R → as ⇉ Set r
-⌊_⌋ {zero}  R? = Lift _ (Dec.True R?)
+⌊_⌋ {zero}  R? = Lift _ (True R?)
 ⌊_⌋ {suc n} R? a = ⌊ R? a ⌋
 
 -- equivalence between R and its erasure
diff --git a/src/Relation/Nullary/Decidable.agda b/src/Relation/Nullary/Decidable.agda
index 37d3e0904a..eefa08c532 100644
--- a/src/Relation/Nullary/Decidable.agda
+++ b/src/Relation/Nullary/Decidable.agda
@@ -9,7 +9,7 @@
 module Relation.Nullary.Decidable where
 
 open import Level using (Level)
-open import Data.Bool.Base using (true; false; if_then_else_)
+open import Data.Bool.Base using (true; false)
 open import Data.Empty using (⊥-elim)
 open import Data.Product.Base as Prod hiding (map)
 open import Data.Sum.Base as Sum hiding (map)
@@ -18,8 +18,8 @@ open import Function.Bundles using
   (Injection; module Injection; module Equivalence; _⇔_; _↔_; mk↔ₛ′)
 open import Relation.Binary.Bundles using (Setoid; module Setoid)
 open import Relation.Binary.Definitions using (Decidable)
-open import Relation.Nullary
-open import Relation.Nullary.Negation
+open import Relation.Nullary using (Irrelevant)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong′)
 
@@ -61,7 +61,7 @@ module _ {a₁ a₂ b₁ b₂} {A : Setoid a₁ a₂} {B : Setoid b₁ b₂}
 
 True-↔ : (dec : Dec P) → Irrelevant P → True dec ↔ P
 True-↔ (true  because  [p]) irr = mk↔ₛ′ (λ _ → invert [p]) _ (irr (invert [p])) cong′
-True-↔ (false because ofⁿ ¬p) _ = mk↔ₛ′ (λ ()) (invert (ofⁿ ¬p)) (⊥-elim ∘ ¬p) λ ()
+True-↔ (false because [¬p]) irr = mk↔ₛ′ (λ ()) (invert [¬p]) (⊥-elim ∘ (invert [¬p])) λ ()
 
 ------------------------------------------------------------------------
 -- Result of decidability
@@ -72,11 +72,11 @@ isYes≗does (false because _) = refl
 
 dec-true : (p? : Dec P) → P → does p? ≡ true
 dec-true (true  because   _ ) p = refl
-dec-true (false because [¬p]) p = ⊥-elim (invert [¬p] p)
+dec-true (false because [¬p]) p = contradiction p (invert [¬p])
 
 dec-false : (p? : Dec P) → ¬ P → does p? ≡ false
 dec-false (false because  _ ) ¬p = refl
-dec-false (true  because [p]) ¬p = ⊥-elim (¬p (invert [p]))
+dec-false (true  because [p]) ¬p = contradiction (invert [p]) ¬p
 
 dec-yes : (p? : Dec P) → P → ∃ λ p′ → p? ≡ yes p′
 dec-yes p? p with dec-true p? p
@@ -87,5 +87,4 @@ dec-no p? ¬p with dec-false p? ¬p
 dec-no (no _) _ | refl = refl
 
 dec-yes-irr : (p? : Dec P) → Irrelevant P → (p : P) → p? ≡ yes p
-dec-yes-irr p? irr p with dec-yes p? p
-... | p′ , eq rewrite irr p p′ = eq
+dec-yes-irr p? irr p with p′ , eq ← dec-yes p? p rewrite irr p p′ = eq
diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index 2d827519d7..aee6ca9d8e 100644
--- a/src/Relation/Nullary/Decidable/Core.agda
+++ b/src/Relation/Nullary/Decidable/Core.agda
@@ -14,7 +14,6 @@ module Relation.Nullary.Decidable.Core where
 open import Level using (Level; Lift)
 open import Data.Bool.Base using (Bool; false; true; not; T; _∧_; _∨_)
 open import Data.Unit.Base using (⊤)
-open import Data.Empty using (⊥)
 open import Data.Empty.Irrelevant using (⊥-elim)
 open import Data.Product.Base using (_×_)
 open import Data.Sum.Base using (_⊎_)
@@ -52,6 +51,12 @@ open Dec public
 pattern yes p =  true because ofʸ  p
 pattern no ¬p = false because ofⁿ ¬p
 
+------------------------------------------------------------------------
+-- Booleans (decision procedures) are Decidable
+
+T? : ∀ b → Dec (T b)
+T? b = b because (T⁺ b)
+
 ------------------------------------------------------------------------
 -- Recompute
 
@@ -168,7 +173,7 @@ proof (map′ P→Q Q→P (false because [¬p])) = ofⁿ (invert [¬p] ∘ Q→P
 
 decidable-stable : Dec P → Stable P
 decidable-stable (yes p) ¬¬p = p
-decidable-stable (no ¬p) ¬¬p = ⊥-elim (¬¬p ¬p)
+decidable-stable (no ¬p) ¬¬p = contradiction ¬p ¬¬p
 
 ¬-drop-Dec : Dec (¬ ¬ P) → Dec (¬ P)
 ¬-drop-Dec ¬¬p? = map′ negated-stable contradiction (¬? ¬¬p?)
@@ -179,7 +184,14 @@ decidable-stable (no ¬p) ¬¬p = ⊥-elim (¬¬p ¬p)
 ¬¬-excluded-middle : DoubleNegation (Dec P)
 ¬¬-excluded-middle ¬h = ¬h (no (λ p → ¬h (yes p)))
 
-excluded-middle : DoubleNegation (Dec P)
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.0
+
 excluded-middle = ¬¬-excluded-middle
 
 {-# WARNING_ON_USAGE excluded-middle
diff --git a/src/Relation/Nullary/Reflects.agda b/src/Relation/Nullary/Reflects.agda
index 66556e8ae6..4c24a964d7 100644
--- a/src/Relation/Nullary/Reflects.agda
+++ b/src/Relation/Nullary/Reflects.agda
@@ -11,13 +11,12 @@ module Relation.Nullary.Reflects where
 open import Agda.Builtin.Equality
 
 open import Data.Bool.Base
-open import Data.Empty
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
 open import Level using (Level)
-open import Function.Base using (_$_; _∘_; const)
+open import Function.Base using (id; _$_; _∘_; const)
 
-open import Relation.Nullary.Negation.Core
+open import Relation.Nullary.Negation.Core using (¬_; contradiction; _¬-⊎_)
 
 private
   variable
@@ -37,6 +36,10 @@ data Reflects {p} (P : Set p) : Bool → Set p where
 ------------------------------------------------------------------------
 -- Constructors and destructors
 
+T⁺ : ∀ b → Reflects (T b) b
+T⁺ true  = ofʸ _
+T⁺ false = ofⁿ id
+
 -- These lemmas are intended to be used mostly when `b` is a value, so
 -- that the `if` expressions have already been evaluated away.
 -- In this case, `of` works like the relevant constructor (`ofⁿ` or
@@ -80,7 +83,7 @@ _→-reflects_ : ∀ {a b} → Reflects P a → Reflects Q b →
                 Reflects (P → Q) (not a ∨ b)
 ofʸ  p →-reflects ofʸ  q = ofʸ (const q)
 ofʸ  p →-reflects ofⁿ ¬q = ofⁿ (¬q ∘ (_$ p))
-ofⁿ ¬p →-reflects _      = ofʸ (⊥-elim ∘ ¬p)
+ofⁿ ¬p →-reflects _      = ofʸ (λ p → contradiction p ¬p)
 
 ------------------------------------------------------------------------
 -- Other lemmas
@@ -92,6 +95,6 @@ fromEquivalence {b = false} sound complete = ofⁿ complete
 -- `Reflects` is deterministic.
 det : ∀ {b b′} → Reflects P b → Reflects P b′ → b ≡ b′
 det (ofʸ  p) (ofʸ  p′) = refl
-det (ofʸ  p) (ofⁿ ¬p′) = ⊥-elim (¬p′ p)
-det (ofⁿ ¬p) (ofʸ  p′) = ⊥-elim (¬p p′)
+det (ofʸ  p) (ofⁿ ¬p′) = contradiction p ¬p′
+det (ofⁿ ¬p) (ofʸ  p′) = contradiction p′ ¬p
 det (ofⁿ ¬p) (ofⁿ ¬p′) = refl
diff --git a/src/Relation/Unary/Polymorphic/Properties.agda b/src/Relation/Unary/Polymorphic/Properties.agda
index 3a59912e2b..d364830ff3 100644
--- a/src/Relation/Unary/Polymorphic/Properties.agda
+++ b/src/Relation/Unary/Polymorphic/Properties.agda
@@ -11,7 +11,7 @@ module Relation.Unary.Polymorphic.Properties where
 
 open import Level using (Level)
 open import Relation.Binary.Definitions hiding (Decidable; Universal)
-open import Relation.Nullary.Decidable using (yes; no)
+open import Relation.Nullary.Decidable.Core using (yes; no)
 open import Relation.Unary hiding (∅; U)
 open import Relation.Unary.Polymorphic
 open import Data.Unit.Polymorphic.Base using (tt)
diff --git a/src/Relation/Unary/Properties.agda b/src/Relation/Unary/Properties.agda
index d090716c08..87dc933e41 100644
--- a/src/Relation/Unary/Properties.agda
+++ b/src/Relation/Unary/Properties.agda
@@ -16,7 +16,7 @@ open import Relation.Binary.Core as Binary
 open import Relation.Binary.Definitions hiding (Decidable; Universal; Irrelevant)
 open import Relation.Binary.PropositionalEquality.Core using (refl)
 open import Relation.Unary
-open import Relation.Nullary.Decidable using (yes; no; _⊎-dec_; _×-dec_; ¬?)
+open import Relation.Nullary.Decidable.Core using (yes; no; _⊎-dec_; _×-dec_; ¬?)
 open import Function.Base using (id; _$_; _∘_)
 
 private
diff --git a/src/System/Clock.agda b/src/System/Clock.agda
index d8b8745b17..9dae2e2e9c 100644
--- a/src/System/Clock.agda
+++ b/src/System/Clock.agda
@@ -21,7 +21,6 @@ open import IO.Base
 open import Function.Base using (_$_; _∘′_)
 open import Foreign.Haskell using (_,_)
 
-open import Relation.Nullary.Decidable using (False; fromWitnessFalse; toWitnessFalse)
 
 private
   variable
diff --git a/src/Tactic/RingSolver.agda b/src/Tactic/RingSolver.agda
index 07e9f1a033..c3cdbaf1ca 100644
--- a/src/Tactic/RingSolver.agda
+++ b/src/Tactic/RingSolver.agda
@@ -20,7 +20,7 @@ open import Data.Unit.Base             using (⊤)
 open import Data.String.Base as String using (String; _++_; parens)
 open import Data.Product.Base          using (_,_; proj₁)
 open import Function.Base
-open import Relation.Nullary.Decidable
+open import Relation.Nullary.Decidable.Core
 
 open import Reflection
 open import Reflection.AST.Argument
diff --git a/src/Test/Golden.agda b/src/Test/Golden.agda
index 43bbd3037e..7e592a3ff2 100644
--- a/src/Test/Golden.agda
+++ b/src/Test/Golden.agda
@@ -97,7 +97,7 @@ open import Data.Unit.Base using (⊤)
 
 open import Function.Base using (id; _$_; case_of_)
 
-open import Relation.Nullary.Decidable using (does)
+open import Relation.Nullary.Decidable.Core using (does)
 
 open import Codata.Musical.Notation using (♯_)
 open import IO
diff --git a/src/Text/Pretty/Core.agda b/src/Text/Pretty/Core.agda
index 974b1af823..8dd947e958 100644
--- a/src/Text/Pretty/Core.agda
+++ b/src/Text/Pretty/Core.agda
@@ -33,7 +33,7 @@ open import Data.String.Base as String
   using (String; length; replicate; _++_; unlines)
 open import Data.String.Unsafe as Stringₚ
 open import Function.Base
-open import Relation.Nullary.Decidable using (Dec)
+open import Relation.Nullary.Decidable.Core using (Dec)
 open import Relation.Unary using (IUniversal; _⇒_; U)
 open import Relation.Binary.PropositionalEquality
 
diff --git a/src/Text/Regex/Derivative/Brzozowski.agda b/src/Text/Regex/Derivative/Brzozowski.agda
index 9c66c831a4..3b2861b06d 100644
--- a/src/Text/Regex/Derivative/Brzozowski.agda
+++ b/src/Text/Regex/Derivative/Brzozowski.agda
@@ -15,9 +15,8 @@ open import Data.List.Relation.Binary.Equality.Propositional
 open import Data.Sum.Base as Sum using (inj₁; inj₂)
 
 open import Function.Base using (_$_; _∘′_; case_of_)
-open import Relation.Nullary.Decidable using (Dec; yes; no)
-open import Relation.Nullary.Negation using (contradiction)
-open import Relation.Nullary.Decidable using (map′; ¬?)
+open import Relation.Nullary.Decidable.Core using (Dec; yes; no; map′; ¬?)
+open import Relation.Nullary.Negation.Core using (contradiction)
 open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
 
diff --git a/src/Text/Regex/Properties.agda b/src/Text/Regex/Properties.agda
index 02b6db2039..48b073ee22 100644
--- a/src/Text/Regex/Properties.agda
+++ b/src/Text/Regex/Properties.agda
@@ -17,9 +17,9 @@ open import Data.Product.Base using (_×_; _,_; uncurry)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Function.Base using (_$_)
 
-open import Relation.Nullary.Decidable
+open import Relation.Nullary.Decidable.Core
   using (Dec; yes; no; map′; ¬?; _×-dec_; _⊎-dec_)
-open import Relation.Nullary.Negation
+open import Relation.Nullary.Negation.Core
   using (¬_; contradiction)
 
 import Relation.Unary  as U
diff --git a/src/Text/Regex/Search.agda b/src/Text/Regex/Search.agda
index efa1f74684..7c6ce741a5 100644
--- a/src/Text/Regex/Search.agda
+++ b/src/Text/Regex/Search.agda
@@ -26,9 +26,8 @@ open import Data.List.Relation.Binary.Pointwise
 open import Data.List.Relation.Binary.Suffix.Heterogeneous
   using (Suffix; here; there) hiding (module Suffix)
 
-open import Relation.Nullary using (Dec; ¬_; yes; no)
-open import Relation.Nullary.Decidable using (map′)
-open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Nullary.Decidable.Core using (Dec; yes; no; map′)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Binary.Core using (Rel; _⇒_)
 open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Binary.PropositionalEquality.Core
diff --git a/src/Text/Regex/SmartConstructors.agda b/src/Text/Regex/SmartConstructors.agda
index 3269d22da5..5d7d8a04d2 100644
--- a/src/Text/Regex/SmartConstructors.agda
+++ b/src/Text/Regex/SmartConstructors.agda
@@ -17,8 +17,8 @@ open import Data.List.Base using ([])
 open import Data.List.Relation.Ternary.Appending.Propositional
 open import Data.Sum.Base using (inj₁; inj₂; fromInj₁; fromInj₂)
 
-open import Relation.Nullary.Decidable using (yes; no)
-open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Nullary.Decidable.Core using (yes; no)
+open import Relation.Nullary.Negation.Core using (contradiction)
 open import Relation.Binary.PropositionalEquality.Core using (refl)
 
 open import Text.Regex.Base P as R hiding (_∣_; _∙_; _⋆)
diff --git a/src/Text/Regex/String/Unsafe.agda b/src/Text/Regex/String/Unsafe.agda
index 118b48505a..ef04bd44a1 100644
--- a/src/Text/Regex/String/Unsafe.agda
+++ b/src/Text/Regex/String/Unsafe.agda
@@ -15,7 +15,7 @@ open import Level using (0ℓ)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; sym; subst)
-open import Relation.Nullary.Decidable using (map′)
+open import Relation.Nullary.Decidable.Core using (map′)
 
 ------------------------------------------------------------------------
 -- Re-exporting safe definitions
diff --git a/tests/data/trie/Main.agda b/tests/data/trie/Main.agda
index 3ce2ad3ecb..2c1feaa7cd 100644
--- a/tests/data/trie/Main.agda
+++ b/tests/data/trie/Main.agda
@@ -19,7 +19,7 @@ open import Data.These        as These
 open import Function.Base using (case_of_; _$_; _∘′_; id; _on_)
 open import Relation.Nary
 open import Relation.Binary.Core using (Rel)
-open import Relation.Nullary.Decidable using (¬?)
+open import Relation.Nullary.Decidable.Core using (¬?)
 
 open import Data.Trie Char.<-strictTotalOrder
 open import Data.Tree.AVL.Value
diff --git a/tests/reflection/assumption/Main.agda b/tests/reflection/assumption/Main.agda
index cf0d21b514..5663c0b524 100644
--- a/tests/reflection/assumption/Main.agda
+++ b/tests/reflection/assumption/Main.agda
@@ -17,7 +17,7 @@ open import Reflection.AST.Literal hiding (_≟_)
 open import Reflection.AST.Argument using (Arg; unArg; arg)
 open import Reflection.AST.DeBruijn
 open import Reflection.AST.Show
-open import Relation.Nullary.Decidable using (does)
+open import Relation.Nullary.Decidable.Core using (does)
 
 open import Effect.Monad
 open RawMonad {{...}}