diff --git a/CHANGELOG.md b/CHANGELOG.md
index d7e1059ccf..daa7facc16 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -90,7 +90,6 @@ Non-backwards compatible changes
   So `[a-zA-Z]+.agdai?` run on "the path _build/Main.agdai corresponds to"
   will return "Main.agdai" when it used to be happy to just return "n.agda".
 
-
 ### Refactoring of algebraic lattice hierarchy
 
 * In order to improve modularity and consistency with `Relation.Binary.Lattice`,
@@ -386,6 +385,31 @@ Non-backwards compatible changes
   * `IsSemiringWithoutAnnihilatingZero*` and `isSemiringWithoutAnnihilatingZero*`
   * `IsRing*` and `isRing*`
 
+### Proof-irrelevant empty type
+
+* The definition of ⊥ has been changed to
+  ```agda
+  private
+    data Empty : Set where
+
+  ⊥ : Set
+  ⊥ = Irrelevant Empty
+  ```
+  in order to make ⊥ proof irrelevant. Any two proofs of `⊥` or of a negated
+  statements are now *judgementally* equal to each other.
+
+* Consequently we have modified the following definitions:
+  + In `Relation.Nullary.Decidable.Core`, the type of `dec-no` has changed
+    ```agda
+    dec-no : (p? : Dec P) → ¬ P → ∃ λ ¬p′ → p? ≡ no ¬p′
+      ↦ dec-no : (p? : Dec P) (¬p : ¬ P) → p? ≡ no ¬p
+    ```
+  + In `Relation.Binary.PropositionalEquality`, the type of `≢-≟-identity` has changed
+    ```agda
+    ≢-≟-identity : x ≢ y → ∃ λ ¬eq → x ≟ y ≡ no ¬eq
+      ↦ ≢-≟-identity : (x≢y : x ≢ y) → x ≟ y ≡ no x≢y
+    ```
+
 ### Other
 
 * The first two arguments of `m≡n⇒m-n≡0` (now `i≡j⇒i-j≡0`) in `Data.Integer.Base`
@@ -602,7 +626,7 @@ Deprecated names
   *-monoˡ-≤-neg    ↦  *-monoˡ-≤-nonPos
   *-cancelˡ-<-neg  ↦  *-cancelˡ-<-nonPos
   *-cancelʳ-<-neg  ↦  *-cancelʳ-<-nonPos
-  
+
   ^-semigroup-morphism ↦ ^-isMagmaHomomorphism
   ^-monoid-morphism    ↦ ^-isMonoidHomomorphism
   ```
@@ -709,6 +733,11 @@ Deprecated names
   invPreorder   ↦ converse-preorder
   ```
 
+### Renamed Data.Erased to Data.Irrelevant
+
+* This fixes the fact we had picked the wrong name originally. The erased modality
+  corresponds to @0 whereas the irrelevance one corresponds to `.`.
+
 New modules
 -----------
 
@@ -1021,7 +1050,7 @@ Other minor changes
   combine-injective  : combine i j ≡ combine k l → i ≡ k × j ≡ l
   combine-surjective : ∀ i → ∃₂ λ j k → combine j k ≡ i
   combine-monoˡ-<    :  i < j → combine i k < combine j l
-  
+
   lower₁-injective   : lower₁ i n≢i ≡ lower₁ j n≢j → i ≡ j
 
   i<1+i              : i < suc i
@@ -1065,7 +1094,7 @@ Other minor changes
   derunᵇ       : (A → A → Bool) → List A → List A
   deduplicateᵇ : (A → A → Bool) → List A → List A
   ```
-  
+
 * Added new proofs in `Data.List.Relation.Binary.Lex.Strict`:
   ```agda
   xs≮[] : ¬ xs < []
@@ -1245,9 +1274,9 @@ Other minor changes
 * Added new functions in `Data.String.Base`:
   ```agda
   wordsByᵇ : (Char → Bool) → String → List String
-  linesByᵇ : (Char → Bool) → String → List String 
+  linesByᵇ : (Char → Bool) → String → List String
   ```
-  
+
 * Added new proofs in `Data.String.Properties`:
   ```
   ≤-isDecTotalOrder-≈ : IsDecTotalOrder _≈_ _≤_
@@ -1488,6 +1517,9 @@ Other minor changes
   ≐′-trans : Trans _≐′_ _≐′_ _≐′_
   ≐⇒≐′ : _≐_ ⇒ _≐′_
   ≐′⇒≐ : _≐′_ ⇒ _≐_
+
+  U-irrelevant : Irrelevant {A = A} U
+  ∁-irrelevant : (P : Pred A ℓ) → Irrelevant (∁ P)
   ```
 
 * Generalised proofs in `Relation.Unary.Properties`:
@@ -1505,7 +1537,7 @@ Other minor changes
   ```
   record ApartnessRelation c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   ```
-  
+
 * Added new definitions in `Relation.Binary.Structures`:
   ```
   record IsApartnessRelation (_#_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
diff --git a/src/Data/Empty.agda b/src/Data/Empty.agda
index decbac8c3e..c232f6ea50 100644
--- a/src/Data/Empty.agda
+++ b/src/Data/Empty.agda
@@ -1,13 +1,15 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Empty type
+-- Empty type, judgementally proof irrelevant
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
 
 module Data.Empty where
 
+open import Data.Irrelevant using (Irrelevant)
+
 ------------------------------------------------------------------------
 -- Definition
 
@@ -15,7 +17,18 @@ module Data.Empty where
 -- often results in unsolved metas. See `Data.Empty.Polymorphic` for a
 -- universe polymorphic variant.
 
-data ⊥ : Set where
+private
+  data Empty : Set where
+
+-- ⊥ is defined via Data.Irrelevant (a record with a single irrelevant field)
+-- so that Agda can judgementally declare that all proofs of ⊥ are equal
+-- to each other. In particular this means that all functions returning a
+-- proof of ⊥ are equal.
+
+⊥ : Set
+⊥ = Irrelevant Empty
+
+{-# DISPLAY Irrelevant Empty = ⊥ #-}
 
 ------------------------------------------------------------------------
 -- Functions
diff --git a/src/Data/Erased.agda b/src/Data/Erased.agda
index 4e74ce3df4..9108b848b0 100644
--- a/src/Data/Erased.agda
+++ b/src/Data/Erased.agda
@@ -1,53 +1,21 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Wrapper for the erased modality
---
--- This allows us to store erased proofs in a record and use projections
--- to manipulate them without having to turn on the unsafe option
--- --irrelevant-projections.
+-- This module is DEPRECATED.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
 
 module Data.Erased where
 
-open import Level using (Level)
-
-private
-  variable
-    a b c : Level
-    A : Set a
-    B : Set b
-    C : Set c
-
-------------------------------------------------------------------------
--- Type
-
-record Erased (A : Set a) : Set a where
-  constructor [_]
-  field .erased : A
-open Erased public
-
-------------------------------------------------------------------------
--- Algebraic structure: Functor, Appplicative and Monad-like
-
-map : (A → B) → Erased A → Erased B
-map f [ a ] = [ f a ]
-
-pure : A → Erased A
-pure x = [ x ]
-
-infixl 4 _<*>_
-_<*>_ : Erased (A → B) → Erased A → Erased B
-[ f ] <*> [ a ] = [ f a ]
-
-infixl 1 _>>=_
-_>>=_ : Erased A → (.A → Erased B) → Erased B
-[ a ] >>= f = f a
-
-------------------------------------------------------------------------
--- Other functions
-
-zipWith : (A → B → C) → Erased A → Erased B → Erased C
-zipWith f a b = ⦇ f a b ⦈
+{-# WARNING_ON_IMPORT
+"Data.Erased was deprecated in v2.0.
+Use Data.Irrelevant instead."
+#-}
+
+open import Data.Irrelevant public
+  using ([_]; map; pure; _<*>_; _>>=_; zipWith)
+  renaming
+  ( Irrelevant to Erased
+  ; irrelevant to erased
+  )
diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda
index 6b71b1c80b..92f0f29db6 100644
--- a/src/Data/Fin/Permutation.agda
+++ b/src/Data/Fin/Permutation.agda
@@ -211,8 +211,10 @@ insert {m} {n} i j π = permutation to from record
   left-inverse-of : ∀ k → from (to k) ≡ k
   left-inverse-of k with i ≟ k
   ... | yes i≡k rewrite proj₂ (dec-yes (j ≟ j) refl) = i≡k
-  ... | no  i≢k with dec-no (j ≟ punchIn j (π ⟨$⟩ʳ punchOut i≢k)) (punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym)
-  ... | j≢punchInⱼπʳpunchOuti≢k , p rewrite p = begin
+  ... | no  i≢k
+    with j≢punchInⱼπʳpunchOuti≢k ← punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym
+    rewrite dec-no (j ≟ punchIn j (π ⟨$⟩ʳ punchOut i≢k)) j≢punchInⱼπʳpunchOuti≢k
+    = begin
     punchIn i (π ⟨$⟩ˡ punchOut j≢punchInⱼπʳpunchOuti≢k)                    ≡⟨ cong (λ l → punchIn i (π ⟨$⟩ˡ l)) (punchOut-cong j refl) ⟩
     punchIn i (π ⟨$⟩ˡ punchOut (punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym)) ≡⟨ cong (λ l → punchIn i (π ⟨$⟩ˡ l)) (punchOut-punchIn j) ⟩
     punchIn i (π ⟨$⟩ˡ (π ⟨$⟩ʳ punchOut i≢k))                              ≡⟨ cong (punchIn i) (inverseˡ π) ⟩
@@ -222,8 +224,10 @@ insert {m} {n} i j π = permutation to from record
   right-inverse-of : ∀ k → to (from k) ≡ k
   right-inverse-of k with j ≟ k
   ... | yes j≡k rewrite proj₂ (dec-yes (i ≟ i) refl) = j≡k
-  ... | no  j≢k with dec-no (i ≟ punchIn i (π ⟨$⟩ˡ punchOut j≢k)) (punchInᵢ≢i i (π ⟨$⟩ˡ punchOut j≢k) ∘ sym)
-  ... | i≢punchInᵢπˡpunchOutj≢k , p rewrite p = begin
+  ... | no  j≢k
+    with i≢punchInᵢπˡpunchOutj≢k ← punchInᵢ≢i i (π ⟨$⟩ˡ punchOut j≢k) ∘ sym
+    rewrite dec-no (i ≟ punchIn i (π ⟨$⟩ˡ punchOut j≢k)) i≢punchInᵢπˡpunchOutj≢k
+    = begin
     punchIn j (π ⟨$⟩ʳ punchOut i≢punchInᵢπˡpunchOutj≢k)                    ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-cong i refl) ⟩
     punchIn j (π ⟨$⟩ʳ punchOut (punchInᵢ≢i i (π ⟨$⟩ˡ punchOut j≢k) ∘ sym)) ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-punchIn i) ⟩
     punchIn j (π ⟨$⟩ʳ (π ⟨$⟩ˡ punchOut j≢k))                              ≡⟨ cong (punchIn j) (inverseʳ π) ⟩
diff --git a/src/Data/Irrelevant.agda b/src/Data/Irrelevant.agda
new file mode 100644
index 0000000000..3c3b25f146
--- /dev/null
+++ b/src/Data/Irrelevant.agda
@@ -0,0 +1,54 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Wrapper for the proof irrelevance modality
+--
+-- This allows us to store proof irrelevant witnesses in a record and
+-- use projections to manipulate them without having to turn on the
+-- unsafe option --irrelevant-projections.
+-- Cf. Data.Refinement for a use case
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Irrelevant where
+
+open import Level using (Level)
+
+private
+  variable
+    a b c : Level
+    A : Set a
+    B : Set b
+    C : Set c
+
+------------------------------------------------------------------------
+-- Type
+
+record Irrelevant (A : Set a) : Set a where
+  constructor [_]
+  field .irrelevant : A
+open Irrelevant public
+
+------------------------------------------------------------------------
+-- Algebraic structure: Functor, Appplicative and Monad-like
+
+map : (A → B) → Irrelevant A → Irrelevant B
+map f [ a ] = [ f a ]
+
+pure : A → Irrelevant A
+pure x = [ x ]
+
+infixl 4 _<*>_
+_<*>_ : Irrelevant (A → B) → Irrelevant A → Irrelevant B
+[ f ] <*> [ a ] = [ f a ]
+
+infixl 1 _>>=_
+_>>=_ : Irrelevant A → (.A → Irrelevant B) → Irrelevant B
+[ a ] >>= f = f a
+
+------------------------------------------------------------------------
+-- Other functions
+
+zipWith : (A → B → C) → Irrelevant A → Irrelevant B → Irrelevant C
+zipWith f a b = ⦇ f a b ⦈
diff --git a/src/Data/Refinement.agda b/src/Data/Refinement.agda
index 3cabaea29b..c06c1e680c 100644
--- a/src/Data/Refinement.agda
+++ b/src/Data/Refinement.agda
@@ -1,7 +1,7 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Refinement type: a value together with an erased proof.
+-- Refinement type: a value together with a proof irrelevant witness.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
@@ -9,9 +9,9 @@
 module Data.Refinement where
 
 open import Level
-open import Data.Erased as Erased using (Erased)
+open import Data.Irrelevant as Irrelevant using (Irrelevant)
 open import Function.Base
-open import Relation.Unary
+open import Relation.Unary using (IUniversal; _⇒_; _⊢_)
 
 private
   variable
@@ -22,7 +22,7 @@ private
 record Refinement {a p} (A : Set a) (P : A → Set p) : Set (a ⊔ p) where
   constructor _,_
   field value : A
-        proof : Erased (P value)
+        proof : Irrelevant (P value)
 open Refinement public
 
 -- The syntax declaration below is meant to mimick set comprehension.
@@ -37,7 +37,7 @@ module _ {P : A → Set p} {Q : B → Set q} where
 
   map : (f : A → B) → ∀[ P ⇒ f ⊢ Q ] →
         [ a ∈ A ∣ P a ] → [ b ∈ B ∣ Q b ]
-  map f prf (a , p) = f a , Erased.map prf p
+  map f prf (a , p) = f a , Irrelevant.map prf p
 
 module _ {P : A → Set p} {Q : A → Set q} where
 
diff --git a/src/Relation/Binary/PropositionalEquality.agda b/src/Relation/Binary/PropositionalEquality.agda
index 72a311bd8b..54081e8afb 100644
--- a/src/Relation/Binary/PropositionalEquality.agda
+++ b/src/Relation/Binary/PropositionalEquality.agda
@@ -113,10 +113,10 @@ cong-≡id {f = f} {x} f≡id =
   f≡id (f x)                                     ∎
   where open ≡-Reasoning; fx≡x = f≡id x; f²x≡x = f≡id (f x)
 
-module _ (_≟_ : Decidable {A = A} _≡_) {x y : A} where
+module _ (_≟_ : DecidableEquality A) {x y : A} where
 
   ≡-≟-identity : (eq : x ≡ y) → x ≟ y ≡ yes eq
   ≡-≟-identity eq = dec-yes-irr (x ≟ y) (Decidable⇒UIP.≡-irrelevant _≟_) eq
 
-  ≢-≟-identity : x ≢ y → ∃ λ ¬eq → x ≟ y ≡ no ¬eq
-  ≢-≟-identity ¬eq = dec-no (x ≟ y) ¬eq
+  ≢-≟-identity : (x≢y : x ≢ y) → x ≟ y ≡ no x≢y
+  ≢-≟-identity = dec-no (x ≟ y)
diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index 11734ac9c7..74974fb351 100644
--- a/src/Relation/Nullary/Decidable/Core.agda
+++ b/src/Relation/Nullary/Decidable/Core.agda
@@ -113,9 +113,9 @@ dec-yes : (p? : Dec P) → P → ∃ λ p′ → p? ≡ yes p′
 dec-yes p? p with dec-true p? p
 dec-yes (yes p′) p | refl = p′ , refl
 
-dec-no : (p? : Dec P) → ¬ P → ∃ λ ¬p′ → p? ≡ no ¬p′
+dec-no : (p? : Dec P) (¬p : ¬ P) → p? ≡ no ¬p
 dec-no p? ¬p with dec-false p? ¬p
-dec-no (no ¬p′) ¬p | refl = ¬p′ , refl
+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
diff --git a/src/Relation/Unary/Properties.agda b/src/Relation/Unary/Properties.agda
index 4044c478d4..225b527b1a 100644
--- a/src/Relation/Unary/Properties.agda
+++ b/src/Relation/Unary/Properties.agda
@@ -8,12 +8,14 @@
 
 module Relation.Unary.Properties where
 
+open import Agda.Builtin.Equality using (refl)
+
 open import Data.Product as Product using (_×_; _,_; swap; proj₁; zip′)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Data.Unit.Base using (tt)
 open import Level
 open import Relation.Binary.Core as Binary
-open import Relation.Binary.Definitions hiding (Decidable; Universal)
+open import Relation.Binary.Definitions hiding (Decidable; Universal; Irrelevant)
 open import Relation.Unary
 open import Relation.Nullary using (yes; no)
 open import Relation.Nullary.Product using (_×-dec_)
@@ -227,3 +229,12 @@ _⊎?_ P? Q? (inj₂ b) = Q? b
 
 _~? : {P : Pred (A × B) ℓ} → Decidable P → Decidable (P ~)
 _~? P? = P? ∘ swap
+
+----------------------------------------------------------------------
+-- Irrelevant properties
+
+U-irrelevant : Irrelevant {A = A} U
+U-irrelevant a b = refl
+
+∁-irrelevant : (P : Pred A ℓ) → Irrelevant (∁ P)
+∁-irrelevant P a b = refl
diff --git a/src/Text/Pretty/Core.agda b/src/Text/Pretty/Core.agda
index fa69acc5e9..e09d9e66b5 100644
--- a/src/Text/Pretty/Core.agda
+++ b/src/Text/Pretty/Core.agda
@@ -13,7 +13,7 @@ module Text.Pretty.Core where
 import Level
 
 open import Data.Bool.Base using (Bool)
-open import Data.Erased    as Erased using (Erased) hiding (module Erased)
+open import Data.Irrelevant as Irrelevant using (Irrelevant) hiding (module Irrelevant)
 open import Data.List.Base as List   using (List; []; _∷_)
 open import Data.Nat.Base            using (ℕ; zero; suc; _+_; _⊔_; _≤_; z≤n)
 open import Data.Nat.Properties
@@ -80,7 +80,7 @@ text s = record
   ; lastWidth = width
   ; last      = s , ⦇ refl ⦈
   ; maxWidth  = width , ⦇ (≤-refl , nothing) ⦈
-  } where width = length s; open Erased
+  } where width = length s; open Irrelevant
 
 ------------------------------------------------------------------------
 -- Empty
@@ -208,7 +208,7 @@ private
     block : [ xs ∈ Content ∣ size xs ≡ height ]
     block .value = vBlock
     block .proof = ⦇ isBlock (Block.block x .proof) (Block.block y .proof) ⦈
-      where open Erased
+      where open Irrelevant
 
     isLastLine : length lastx ≡ x.lastWidth →
                  length lasty ≡ y.lastWidth →
@@ -226,7 +226,7 @@ private
     last : [ s ∈ String ∣ length s ≡ lastWidth ]
     last .value = vLast
     last .proof = ⦇ isLastLine (Block.last x .proof) (Block.last y .proof) ⦈
-      where open Erased
+      where open Irrelevant
 
     vMaxWidth : ℕ
     vMaxWidth = widthx ⊔ (x.lastWidth + widthy)
@@ -278,7 +278,7 @@ private
                           (map proj₂ (Block.maxWidth x .proof))
                           (map proj₂ (Block.maxWidth y .proof))
             ⦈
-      ⦈ where open Erased
+      ⦈ where open Irrelevant
 
 infixl 4 _<>_
 _<>_ : Block → Block → Block
@@ -301,7 +301,7 @@ private
     vMaxWidth = widthx
 
     last : [ s ∈ String ∣ length s ≡ lastWidth ]
-    last = "" , ⦇ refl ⦈ where open Erased
+    last = "" , ⦇ refl ⦈ where open Irrelevant
 
     vContent = node? blockx lastx (leaf tt)
 
@@ -314,7 +314,7 @@ private
 
     block : [ xs ∈ Content ∣ size xs ≡ height ]
     block .value = vContent
-    block .proof = Erased.map isBlock $ Block.block x .proof
+    block .proof = Irrelevant.map isBlock $ Block.block x .proof
 
     maxWidth : [ n ∈ ℕ ∣ lastWidth ≤ n × All≤ n vContent ]
     maxWidth .value = widthx
@@ -324,7 +324,7 @@ private
                    (pure (leaf tt))
       ⦈ where
 
-      open Erased
+      open Irrelevant
 
       middle : length lastx ≡ x.lastWidth → x.lastWidth ≤ vMaxWidth →
                length lastx ≤ vMaxWidth