From 7fd48d02404c4727e58b5715af29692aefdab14e Mon Sep 17 00:00:00 2001
From: Tsung-Ju Chiang <71379180+tsung-ju@users.noreply.github.com>
Date: Mon, 2 Dec 2024 02:31:01 +0000
Subject: [PATCH] =?UTF-8?q?Add=20`=E2=89=A4=E2=80=B4-irrelevant`=20to=20`D?=
 =?UTF-8?q?ata.Nat.Properties`=20(#2503)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* Add `≤‴-irrelevant` to `Data.Nat.Properties`

* Add <‴-irrefl and refactor using cong

* Minor simplifications

* Add to CHANGELOG
---
 CHANGELOG.md                 |  5 +++++
 src/Data/Nat/Properties.agda | 21 +++++++++++++++++++++
 2 files changed, 26 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index a58227662c..2f5b9ff7da 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -322,6 +322,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`
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index b7a7c00511..68efe6bcdf 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -2237,6 +2237,27 @@ _>‴?_ = flip _<‴?_
 ≤‴⇒≤ : _≤‴_ ⇒ _≤_
 ≤‴⇒≤ = ≤″⇒≤ ∘ ≤‴⇒≤″
 
+<‴-irrefl : Irreflexive _≡_ _<‴_
+<‴-irrefl eq = <-irrefl eq ∘ ≤‴⇒≤
+
+≤‴-irrelevant : Irrelevant {A = ℕ} _≤‴_
+≤‴-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) 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
+
+>‴-irrelevant : Irrelevant {A = ℕ} _>‴_
+>‴-irrelevant = ≤‴-irrelevant
+
+≥‴-irrelevant : Irrelevant {A = ℕ} _≥‴_
+≥‴-irrelevant = ≤‴-irrelevant
+
 ------------------------------------------------------------------------
 -- Other properties
 ------------------------------------------------------------------------