From b614e441854fdff5f025398a76ed3a65f7249ff3 Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Fri, 14 Mar 2025 17:18:38 -0400
Subject: [PATCH 1/7] New file Irrelevant
---
.../Fresh/Membership/Setoid/Properties.agda | 2 +-
src/Data/List/Relation/Binary/Pointwise.agda | 19 +++++++++++-------
src/Data/List/Relation/Unary/All.agda | 5 +++--
src/Data/Maybe/Relation/Unary/Any.agda | 3 +--
src/Data/Nat/Properties.agda | 6 +++---
src/Data/Unit/Properties.agda | 4 +++-
.../Vec/Relation/Binary/Lex/NonStrict.agda | 2 +-
.../Construct/Add/Infimum/NonStrict.agda | 2 +-
.../Binary/Construct/Add/Infimum/Strict.agda | 3 +--
.../Binary/HeterogeneousEquality.agda | 5 +++--
.../Binary/PropositionalEquality.agda | 2 +-
src/Relation/Nullary.agda | 7 +------
src/Relation/Nullary/Decidable.agda | 2 +-
src/Relation/Nullary/Irrelevant.agda | 20 +++++++++++++++++++
14 files changed, 52 insertions(+), 30 deletions(-)
create mode 100644 src/Relation/Nullary/Irrelevant.agda
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..0c7a0e8f22 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)
@@ -248,3 +248,4 @@ all = all?
"Warning: all was deprecated in v1.4.
Please use all? instead."
#-}
+
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..03d68beb75
--- /dev/null
+++ b/src/Relation/Nullary/Irrelevant.agda
@@ -0,0 +1,20 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Operations on nullary relations (like negation and decidability)
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Relation.Nullary.Irrelevant where
+
+open import Agda.Builtin.Equality using (_≡_)
+open import Level using (Level)
+
+private
+ variable
+ p : Level
+ P : Set p
+
+Irrelevant : Set p → Set p
+Irrelevant P = ∀ (p₁ p₂ : P) → p₁ ≡ p₂
From 7310c436a83a4b564e88a997b09f7b38f5d17b6b Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Fri, 14 Mar 2025 18:08:31 -0400
Subject: [PATCH 2/7] Module Irrelevant description
---
src/Relation/Nullary/Irrelevant.agda | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/src/Relation/Nullary/Irrelevant.agda b/src/Relation/Nullary/Irrelevant.agda
index 03d68beb75..4191bf6d07 100644
--- a/src/Relation/Nullary/Irrelevant.agda
+++ b/src/Relation/Nullary/Irrelevant.agda
@@ -1,7 +1,8 @@
------------------------------------------------------------------------
-- The Agda standard library
--
--- Operations on nullary relations (like negation and decidability)
+-- 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 #-}
From e769d610301d406030c843ed429a440a4be55405 Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Fri, 14 Mar 2025 18:19:31 -0400
Subject: [PATCH 3/7] add Irrelevant file in CHANGELOG
---
CHANGELOG.md | 2 ++
1 file changed, 2 insertions(+)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 76e6a12c76..8ad2ca961a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -120,6 +120,8 @@ New modules
* `Data.Sign.Show` to show a sign
+* `Relation.Nullary.Irrelevant` defining the concept of irrelevance (h-proposition), where all elements of a type are equal.
+
Additions to existing modules
-----------------------------
From 41054aaf2209f20b82e2c9fdca70a50098c7ec16 Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Fri, 14 Mar 2025 18:21:14 -0400
Subject: [PATCH 4/7] remove blank line
---
src/Data/List/Relation/Unary/All.agda | 1 -
1 file changed, 1 deletion(-)
diff --git a/src/Data/List/Relation/Unary/All.agda b/src/Data/List/Relation/Unary/All.agda
index 0c7a0e8f22..eb9438fec7 100644
--- a/src/Data/List/Relation/Unary/All.agda
+++ b/src/Data/List/Relation/Unary/All.agda
@@ -248,4 +248,3 @@ all = all?
"Warning: all was deprecated in v1.4.
Please use all? instead."
#-}
-
From 1d7e87e0cc26090b3b2829ca609264114a362b48 Mon Sep 17 00:00:00 2001
From: Jacques Carette <carette@mcmaster.ca>
Date: Sat, 15 Mar 2025 09:53:17 -0400
Subject: [PATCH 5/7] Update src/Relation/Nullary/Irrelevant.agda
Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
---
src/Relation/Nullary/Irrelevant.agda | 1 -
1 file changed, 1 deletion(-)
diff --git a/src/Relation/Nullary/Irrelevant.agda b/src/Relation/Nullary/Irrelevant.agda
index 4191bf6d07..99b1b48674 100644
--- a/src/Relation/Nullary/Irrelevant.agda
+++ b/src/Relation/Nullary/Irrelevant.agda
@@ -15,7 +15,6 @@ open import Level using (Level)
private
variable
p : Level
- P : Set p
Irrelevant : Set p → Set p
Irrelevant P = ∀ (p₁ p₂ : P) → p₁ ≡ p₂
From 84f8facd0312c421542ab25d81c8a31034105675 Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Mon, 17 Mar 2025 13:19:14 -0400
Subject: [PATCH 6/7] Fix
---
CHANGELOG.md | 5 +++--
1 file changed, 3 insertions(+), 2 deletions(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 8ad2ca961a..91a1c6a169 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -28,6 +28,9 @@ Non-backwards compatible changes
Minor improvements
------------------
+* Moved the concept of irrelevance (h-proposition) from `Relation.Nullary` to
+ its own dedicated module `Relation.Nullary.Irrelevant`.
+
Deprecated modules
------------------
@@ -120,8 +123,6 @@ New modules
* `Data.Sign.Show` to show a sign
-* `Relation.Nullary.Irrelevant` defining the concept of irrelevance (h-proposition), where all elements of a type are equal.
-
Additions to existing modules
-----------------------------
From 38b18247dc0263b2991b0c93966595808cd9b969 Mon Sep 17 00:00:00 2001
From: Jacques <149587529+jmougeot@users.noreply.github.com>
Date: Mon, 17 Mar 2025 15:59:47 -0400
Subject: [PATCH 7/7] Update CHANGELOG.md
Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
---
CHANGELOG.md | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 91a1c6a169..2959d3d6ce 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -28,8 +28,8 @@ Non-backwards compatible changes
Minor improvements
------------------
-* Moved the concept of irrelevance (h-proposition) from `Relation.Nullary` to
- its own dedicated module `Relation.Nullary.Irrelevant`.
+* Moved the concept `Irrelevant` of irrelevance (h-proposition) from `Relation.Nullary`
+ to its own dedicated module `Relation.Nullary.Irrelevant`.
Deprecated modules
------------------