From 350789cb360a05c359559804cdbd50288b19a6b3 Mon Sep 17 00:00:00 2001
From: Tsung-Ju Chiang <71379180+tsung-ju@users.noreply.github.com>
Date: Sat, 23 Nov 2024 00:12:58 -0500
Subject: [PATCH 1/4] =?UTF-8?q?Add=20`=E2=89=A4=E2=80=B4-irrelevant`=20to?=
 =?UTF-8?q?=20`Data.Nat.Properties`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Data/Nat/Properties.agda | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index b7a7c00511..b1f2f053a3 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -2237,6 +2237,24 @@ _>‴?_ = flip _<‴?_
 ≤‴⇒≤ : _≤‴_ ⇒ _≤_
 ≤‴⇒≤ = ≤″⇒≤ ∘ ≤‴⇒≤″
 
+≤‴-irrelevant : Irrelevant {A = ℕ} _≤‴_
+≤‴-irrelevant ≤‴-refl q = lemma q refl
+  where
+  lemma : ∀ {m n} → (p : m ≤‴ n) → (e : m ≡ n) → subst (m ≤‴_) e ≤‴-refl ≡ p
+  lemma ≤‴-refl       e rewrite ≡-irrelevant e refl = refl
+  lemma (≤‴-step m<m) refl = contradiction (≤‴⇒≤ m<m) (<-irrefl refl)
+≤‴-irrelevant (≤‴-step x<x) ≤‴-refl = contradiction (≤‴⇒≤ x<x) (<-irrefl refl)
+≤‴-irrelevant (≤‴-step p)   (≤‴-step q) rewrite ≤‴-irrelevant p q = refl
+
+<‴-irrelevant : Irrelevant {A = ℕ} _<‴_
+<‴-irrelevant = ≤‴-irrelevant
+
+>‴-irrelevant : Irrelevant {A = ℕ} _>‴_
+>‴-irrelevant = ≤‴-irrelevant
+
+≥‴-irrelevant : Irrelevant {A = ℕ} _≥‴_
+≥‴-irrelevant = ≤‴-irrelevant
+
 ------------------------------------------------------------------------
 -- Other properties
 ------------------------------------------------------------------------

From 1a4e923fdb2fa135f10c275e800394f21268f1bc Mon Sep 17 00:00:00 2001
From: Tsung-Ju Chiang <71379180+tsung-ju@users.noreply.github.com>
Date: Sat, 23 Nov 2024 12:52:20 -0500
Subject: [PATCH 2/4] =?UTF-8?q?Add=20<=E2=80=B4-irrefl=20and=20refactor=20?=
 =?UTF-8?q?using=20cong?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Data/Nat/Properties.agda | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index b1f2f053a3..9e6085c716 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -2237,14 +2237,17 @@ _>‴?_ = flip _<‴?_
 ≤‴⇒≤ : _≤‴_ ⇒ _≤_
 ≤‴⇒≤ = ≤″⇒≤ ∘ ≤‴⇒≤″
 
+<‴-irrefl : Irreflexive _≡_ _<‴_
+<‴-irrefl eq = <-irrefl eq ∘ ≤‴⇒≤
+
 ≤‴-irrelevant : Irrelevant {A = ℕ} _≤‴_
-≤‴-irrelevant ≤‴-refl q = lemma q refl
+≤‴-irrelevant ≤‴-refl = lemma refl
   where
-  lemma : ∀ {m n} → (p : m ≤‴ n) → (e : m ≡ n) → subst (m ≤‴_) e ≤‴-refl ≡ p
-  lemma ≤‴-refl       e rewrite ≡-irrelevant e refl = refl
-  lemma (≤‴-step m<m) refl = contradiction (≤‴⇒≤ m<m) (<-irrefl refl)
-≤‴-irrelevant (≤‴-step x<x) ≤‴-refl = contradiction (≤‴⇒≤ x<x) (<-irrefl refl)
-≤‴-irrelevant (≤‴-step p)   (≤‴-step q) rewrite ≤‴-irrelevant p q = refl
+  lemma : ∀ {m n} → (e : m ≡ n) → (q : m ≤‴ n) → subst (m ≤‴_) e ≤‴-refl ≡ q
+  lemma {m} e    ≤‴-refl       = cong (λ e → subst (m ≤‴_) e ≤‴-refl) (≡-irrelevant e refl)
+  lemma     refl (≤‴-step m<m) = contradiction m<m (<‴-irrefl refl)
+≤‴-irrelevant (≤‴-step x<x) ≤‴-refl     = contradiction x<x (<‴-irrefl refl)
+≤‴-irrelevant (≤‴-step p)   (≤‴-step q) = cong ≤‴-step (≤‴-irrelevant p q)
 
 <‴-irrelevant : Irrelevant {A = ℕ} _<‴_
 <‴-irrelevant = ≤‴-irrelevant

From 7116ae4810a0231398c8af2772ce173fe3a3aa3e Mon Sep 17 00:00:00 2001
From: Tsung-Ju Chiang <71379180+tsung-ju@users.noreply.github.com>
Date: Sat, 23 Nov 2024 13:35:06 -0500
Subject: [PATCH 3/4] Minor simplifications

---
 src/Data/Nat/Properties.agda | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 9e6085c716..68efe6bcdf 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -2244,10 +2244,10 @@ _>‴?_ = flip _<‴?_
 ≤‴-irrelevant ≤‴-refl = lemma refl
   where
   lemma : ∀ {m n} → (e : m ≡ n) → (q : m ≤‴ n) → subst (m ≤‴_) e ≤‴-refl ≡ q
-  lemma {m} e    ≤‴-refl       = cong (λ e → subst (m ≤‴_) e ≤‴-refl) (≡-irrelevant e refl)
-  lemma     refl (≤‴-step m<m) = contradiction m<m (<‴-irrefl refl)
-≤‴-irrelevant (≤‴-step x<x) ≤‴-refl     = contradiction x<x (<‴-irrefl refl)
-≤‴-irrelevant (≤‴-step p)   (≤‴-step q) = cong ≤‴-step (≤‴-irrelevant p q)
+  lemma {m} e    ≤‴-refl       = cong (λ e → subst (m ≤‴_) e ≤‴-refl) $ ≡-irrelevant e refl
+  lemma     refl (≤‴-step m<m) with () ← <‴-irrefl refl m<m
+≤‴-irrelevant (≤‴-step m<m) ≤‴-refl     with () ← <‴-irrefl refl m<m
+≤‴-irrelevant (≤‴-step p)   (≤‴-step q) = cong ≤‴-step $ ≤‴-irrelevant p q
 
 <‴-irrelevant : Irrelevant {A = ℕ} _<‴_
 <‴-irrelevant = ≤‴-irrelevant

From 39314b83e472a9f66e4b58361808cdce3ebf3de3 Mon Sep 17 00:00:00 2001
From: Tsung-Ju Chiang <71379180+tsung-ju@users.noreply.github.com>
Date: Sat, 23 Nov 2024 18:00:19 -0500
Subject: [PATCH 4/4] Add to CHANGELOG

---
 CHANGELOG.md | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index f3e17fa961..ddb43446c0 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -318,6 +318,11 @@ Additions to existing modules
   ```agda
   m≤n⇒m≤n*o : ∀ o .{{_ : NonZero o}} → m ≤ n → m ≤ n * o
   m≤n⇒m≤o*n : ∀ o .{{_ : NonZero o}} → m ≤ n → m ≤ o * n
+  <‴-irrefl : Irreflexive _≡_ _<‴_
+  ≤‴-irrelevant : Irrelevant {A = ℕ} _≤‴_
+  <‴-irrelevant : Irrelevant {A = ℕ} _<‴_
+  >‴-irrelevant : Irrelevant {A = ℕ} _>‴_
+  ≥‴-irrelevant : Irrelevant {A = ℕ} _≥‴_
   ```
 
   adjunction between `suc` and `pred`