diff --git a/CHANGELOG.md b/CHANGELOG.md
index 76e6a12c76..2959d3d6ce 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -28,6 +28,9 @@ Non-backwards compatible changes
 Minor improvements
 ------------------
 
+* Moved the concept `Irrelevant` of irrelevance (h-proposition) from `Relation.Nullary`
+  to its own dedicated module `Relation.Nullary.Irrelevant`.
+
 Deprecated modules
 ------------------
 
diff --git a/src/Data/List/Fresh/Membership/Setoid/Properties.agda b/src/Data/List/Fresh/Membership/Setoid/Properties.agda
index b3e107041b..56effd841a 100644
--- a/src/Data/List/Fresh/Membership/Setoid/Properties.agda
+++ b/src/Data/List/Fresh/Membership/Setoid/Properties.agda
@@ -26,7 +26,7 @@ open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; fromInj₂)
 open import Function.Base using (id; _∘′_; _$_)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Nullary.Negation.Core using (¬_)
-open import Relation.Nullary using (Irrelevant)
+open import Relation.Nullary.Irrelevant using (Irrelevant)
 open import Relation.Unary as Unary using (Pred)
 import Relation.Binary.Definitions as Binary using (_Respectsˡ_; Irrelevant)
 import Relation.Binary.PropositionalEquality.Core as ≡
diff --git a/src/Data/List/Relation/Binary/Pointwise.agda b/src/Data/List/Relation/Binary/Pointwise.agda
index 8dda6fa67f..91ed2eb1c5 100644
--- a/src/Data/List/Relation/Binary/Pointwise.agda
+++ b/src/Data/List/Relation/Binary/Pointwise.agda
@@ -18,19 +18,24 @@ open import Data.List.Properties using (≡-dec; length-++)
 open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
 open import Data.List.Relation.Unary.AllPairs using (AllPairs; []; _∷_)
 open import Data.List.Relation.Unary.Any using (Any; here; there)
-open import Data.Fin.Base using (Fin; toℕ; cast) renaming (zero to fzero; suc to fsuc)
+open import Data.Fin.Base
+  using (Fin; toℕ; cast)
+  renaming (zero to fzero; suc to fsuc)
 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 Level using (Level; _⊔_)
 open import Relation.Binary.Core renaming (Rel to Rel₂)
-open import Relation.Binary.Definitions using (Reflexive; _Respects_; _Respects₂_)
+open import Relation.Binary.Definitions
+  using (Reflexive; _Respects_; _Respects₂_)
 open import Relation.Binary.Bundles using (Setoid; DecSetoid; Preorder; Poset)
-open import Relation.Binary.Structures using (IsEquivalence; IsDecEquivalence; IsPartialOrder; IsPreorder)
+open import Relation.Binary.Structures
+  using (IsEquivalence; IsDecEquivalence; IsPartialOrder; IsPreorder)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 import Relation.Binary.PropositionalEquality.Properties as ≡
+open import Relation.Nullary.Decidable as Dec
+  using (map′; yes; no; Dec; _because_)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
+open import Relation.Unary as U using (Pred)
 
 private
   variable
diff --git a/src/Data/List/Relation/Unary/All.agda b/src/Data/List/Relation/Unary/All.agda
index 86a59aca14..eb9438fec7 100644
--- a/src/Data/List/Relation/Unary/All.agda
+++ b/src/Data/List/Relation/Unary/All.agda
@@ -19,8 +19,8 @@ open import Effect.Applicative
 open import Effect.Monad
 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 as Dec
+  using (_×-dec_; yes; no; map′)
 open import Relation.Unary hiding (_∈_)
 import Relation.Unary.Properties as Unary
 open import Relation.Binary.Bundles using (Setoid)
diff --git a/src/Data/Maybe/Relation/Unary/Any.agda b/src/Data/Maybe/Relation/Unary/Any.agda
index d4062e8b81..b35d033588 100644
--- a/src/Data/Maybe/Relation/Unary/Any.agda
+++ b/src/Data/Maybe/Relation/Unary/Any.agda
@@ -16,8 +16,7 @@ open import Level using (Level; _⊔_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)
 open import Relation.Unary
   using (Pred; _⊆_; _∩_; Decidable; Irrelevant; Satisfiable)
-open import Relation.Nullary hiding (Irrelevant)
-import Relation.Nullary.Decidable as Dec using (Dec; yes; no; map)
+open import Relation.Nullary.Decidable as Dec using (Dec; yes; no)
 
 ------------------------------------------------------------------------
 -- Definition
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 11037bc5ae..5cadc91273 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -44,11 +44,11 @@ open import Relation.Binary.Core
 open import Relation.Binary
 open import Relation.Binary.Consequences using (flip-Connex; wlog)
 open import Relation.Binary.PropositionalEquality
-open import Relation.Nullary hiding (Irrelevant)
 open import Relation.Nullary.Decidable
-  using (True; via-injection; map′; recompute)
+  using (True; via-injection; map′; recompute; no; yes; Dec; _because_)
 open import Relation.Nullary.Negation.Core using (¬_; contradiction)
-open import Relation.Nullary.Reflects using (fromEquivalence)
+open import Relation.Nullary.Reflects
+  using (fromEquivalence; Reflects; invert)
 
 open import Algebra.Definitions {A = ℕ} _≡_
   hiding (LeftCancellative; RightCancellative; Cancellative)
diff --git a/src/Data/Unit/Properties.agda b/src/Data/Unit/Properties.agda
index 7c0cb90593..d93055db8d 100644
--- a/src/Data/Unit/Properties.agda
+++ b/src/Data/Unit/Properties.agda
@@ -11,7 +11,6 @@ module Data.Unit.Properties where
 open import Data.Sum.Base using (inj₁)
 open import Data.Unit.Base using (⊤)
 open import Level using (0ℓ)
-open import Relation.Nullary using (Irrelevant; yes)
 open import Relation.Binary.Bundles
   using (Setoid; DecSetoid; Poset; DecTotalOrder)
 open import Relation.Binary.Structures
@@ -22,6 +21,9 @@ open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; refl; trans)
 open import Relation.Binary.PropositionalEquality.Properties
   using (setoid; decSetoid; isEquivalence)
+open import Relation.Nullary.Decidable.Core using (yes)
+open import Relation.Nullary.Irrelevant using (Irrelevant)
+
 
 ------------------------------------------------------------------------
 -- Irrelevancy
diff --git a/src/Data/Vec/Relation/Binary/Lex/NonStrict.agda b/src/Data/Vec/Relation/Binary/Lex/NonStrict.agda
index 680cbadb89..24bee076ef 100644
--- a/src/Data/Vec/Relation/Binary/Lex/NonStrict.agda
+++ b/src/Data/Vec/Relation/Binary/Lex/NonStrict.agda
@@ -33,7 +33,7 @@ open import Relation.Binary.Definitions
   using (Irreflexive; _Respects₂_; Antisymmetric; Asymmetric; Symmetric; Trans
         ; Decidable; Total; Trichotomous)
 import Relation.Binary.Construct.NonStrictToStrict as Conv
-open import Relation.Nullary hiding (Irrelevant)
+open import Relation.Nullary.Decidable.Core using (yes; no)
 
 private
   variable
diff --git a/src/Relation/Binary/Construct/Add/Infimum/NonStrict.agda b/src/Relation/Binary/Construct/Add/Infimum/NonStrict.agda
index 3a76f4601d..b6b0ee8d27 100644
--- a/src/Relation/Binary/Construct/Add/Infimum/NonStrict.agda
+++ b/src/Relation/Binary/Construct/Add/Infimum/NonStrict.agda
@@ -28,8 +28,8 @@ open import Relation.Binary.Structures
         ; IsDecTotalOrder)
 open import Relation.Binary.Definitions
   using (Minimum; Transitive; Total; Decidable; Irrelevant; Antisymmetric)
-open import Relation.Nullary hiding (Irrelevant)
 open import Relation.Nullary.Construct.Add.Infimum using (⊥₋; [_]; _₋; ≡-dec)
+open import Relation.Nullary.Decidable.Core using (yes; no; map′)
 import Relation.Nullary.Decidable.Core as Dec using (map′)
 
 ------------------------------------------------------------------------
diff --git a/src/Relation/Binary/Construct/Add/Infimum/Strict.agda b/src/Relation/Binary/Construct/Add/Infimum/Strict.agda
index fb7dd42acc..122cdd0e1c 100644
--- a/src/Relation/Binary/Construct/Add/Infimum/Strict.agda
+++ b/src/Relation/Binary/Construct/Add/Infimum/Strict.agda
@@ -30,10 +30,9 @@ open import Relation.Binary.Structures
 open import Relation.Binary.Definitions
   using (Asymmetric; Transitive; Decidable; Irrelevant; Irreflexive; Trans
         ; Trichotomous; tri≈; tri<; tri>; _Respectsˡ_; _Respectsʳ_; _Respects₂_)
-open import Relation.Nullary hiding (Irrelevant)
 open import Relation.Nullary.Construct.Add.Infimum
   using (⊥₋; [_]; _₋; ≡-dec; []-injective)
-import Relation.Nullary.Decidable.Core as Dec using (map′)
+open import Relation.Nullary.Decidable.Core as Dec using (yes; no; map′)
 
 ------------------------------------------------------------------------
 -- Definition
diff --git a/src/Relation/Binary/HeterogeneousEquality.agda b/src/Relation/Binary/HeterogeneousEquality.agda
index 8d69c16b6b..6761bea53a 100644
--- a/src/Relation/Binary/HeterogeneousEquality.agda
+++ b/src/Relation/Binary/HeterogeneousEquality.agda
@@ -12,8 +12,6 @@ open import Data.Product.Base using (_,_)
 open import Function.Base using (case_of_; _∋_; id)
 open import Function.Bundles using (Inverse)
 open import Level using (Level; _⊔_)
-open import Relation.Nullary hiding (Irrelevant)
-open import Relation.Unary using (Pred)
 open import Relation.Binary.Core using (Rel; REL; _⇒_)
 open import Relation.Binary.Bundles using (Setoid; DecSetoid; Preorder)
 open import Relation.Binary.Structures using (IsEquivalence; IsPreorder)
@@ -26,6 +24,9 @@ open import Relation.Binary.Indexed.Heterogeneous.Construct.At
   using (_atₛ_)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; refl)
 open import Relation.Binary.Reasoning.Syntax
+open import Relation.Nullary.Decidable.Core using (yes; no)
+open import Relation.Nullary.Negation.Core using (¬_)
+open import Relation.Unary using (Pred)
 
 import Relation.Binary.PropositionalEquality.Properties as ≡
 import Relation.Binary.HeterogeneousEquality.Core as Core
diff --git a/src/Relation/Binary/PropositionalEquality.agda b/src/Relation/Binary/PropositionalEquality.agda
index d84dd0a162..283623cc96 100644
--- a/src/Relation/Binary/PropositionalEquality.agda
+++ b/src/Relation/Binary/PropositionalEquality.agda
@@ -13,7 +13,7 @@ open import Function.Base using (id; _∘_)
 import Function.Dependent.Bundles as Dependent using (Func)
 open import Function.Indexed.Relation.Binary.Equality using (≡-setoid)
 open import Level using (Level; _⊔_)
-open import Relation.Nullary using (Irrelevant)
+open import Relation.Nullary.Irrelevant using (Irrelevant)
 open import Relation.Nullary.Decidable using (yes; no; dec-yes-irr; dec-no)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Definitions using (DecidableEquality)
diff --git a/src/Relation/Nullary.agda b/src/Relation/Nullary.agda
index 5ea302fd98..d2c2eebd84 100644
--- a/src/Relation/Nullary.agda
+++ b/src/Relation/Nullary.agda
@@ -27,12 +27,7 @@ open import Relation.Nullary.Recomputable public using (Recomputable)
 open import Relation.Nullary.Negation.Core public
 open import Relation.Nullary.Reflects public hiding (recompute; recompute-constant)
 open import Relation.Nullary.Decidable.Core public
-
-------------------------------------------------------------------------
--- Irrelevant types
-
-Irrelevant : Set p → Set p
-Irrelevant P = ∀ (p₁ p₂ : P) → p₁ ≡ p₂
+open import Relation.Nullary.Irrelevant public
 
 ------------------------------------------------------------------------
 -- Weak decidability
diff --git a/src/Relation/Nullary/Decidable.agda b/src/Relation/Nullary/Decidable.agda
index 33fd131be6..7c0137b830 100644
--- a/src/Relation/Nullary/Decidable.agda
+++ b/src/Relation/Nullary/Decidable.agda
@@ -15,7 +15,7 @@ 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 using (Irrelevant)
+open import Relation.Nullary.Irrelevant using (Irrelevant)
 open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Binary.PropositionalEquality.Core
diff --git a/src/Relation/Nullary/Irrelevant.agda b/src/Relation/Nullary/Irrelevant.agda
new file mode 100644
index 0000000000..99b1b48674
--- /dev/null
+++ b/src/Relation/Nullary/Irrelevant.agda
@@ -0,0 +1,20 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- A type `A` is irrelevant if all of its elements are equal.
+-- This is also refered to as "A is an h-proposition".
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Relation.Nullary.Irrelevant where
+
+open import Agda.Builtin.Equality using (_≡_)
+open import Level using (Level)
+
+private
+  variable
+    p : Level
+
+Irrelevant : Set p → Set p
+Irrelevant P = ∀ (p₁ p₂ : P) → p₁ ≡ p₂