From 36a7f7cf59bb3d5ba6b058e11bdb186853b14a5c Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 26 Jul 2026 13:31:50 +0100
Subject: [PATCH 1/5] [ add ] more properties of
 `Data.List.Relation.Unary.All.Null`

---
 CHANGELOG.md                                     |  7 +++++++
 src/Data/List/Relation/Unary/All/Properties.agda | 14 +++++++++++++-
 2 files changed, 20 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2c78b4f95a..2215a2f227 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -423,6 +423,13 @@ Additions to existing modules
            ∃[ xs ] Appending as bs xs × Appending xs cs ds
   ```
 
+* In `Data.List.Relation.Unary.All.Properties`:
+  ```agda
+  null-∷          : Null (x ∷ xs) → Whatever
+  null?           : Decidable Null
+  null-irrelevant : Irrelevant Null
+  ```
+
 * In `Data.Nat.DivMod`:
   ```agda
   m<suc[m/n]*n : ∀ m n → m < suc (m / n) * n
diff --git a/src/Data/List/Relation/Unary/All/Properties.agda b/src/Data/List/Relation/Unary/All/Properties.agda
index 6e60adda3e..e21a771eac 100644
--- a/src/Data/List/Relation/Unary/All/Properties.agda
+++ b/src/Data/List/Relation/Unary/All/Properties.agda
@@ -47,7 +47,7 @@ open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Nullary.Decidable
   using (Dec; does; yes; no; _because_; ¬?; decidable-stable; dec-true)
 open import Relation.Unary
-  using (Decidable; Pred; ∁; _⟨×⟩_) renaming (_⊆_ to _⋐_)
+  using (Decidable; Irrelevant; Pred; ∁; _⟨×⟩_) renaming (_⊆_ to _⋐_)
 open import Relation.Unary.Properties using (∁?)
 
 private
@@ -61,6 +61,8 @@ private
     R : Pred C r
     x y : A
     xs ys : List A
+    Whatever : Set _
+
 
 ------------------------------------------------------------------------
 -- Re-export Core Properties
@@ -77,6 +79,16 @@ null⇒Null : T (null xs) → Null xs
 null⇒Null {xs = []   } _ = []
 null⇒Null {xs = _ ∷ _} ()
 
+null-∷ : Null (x ∷ xs) → Whatever
+null-∷ (() ∷ _)
+
+null? : Decidable (Null {A = A})
+null? []      = yes []
+null? (_ ∷ _) = no null-∷
+
+null-irrelevant : Irrelevant (Null {A = A})
+null-irrelevant [] [] = refl
+
 ------------------------------------------------------------------------
 -- Properties of the "points-to" relation _[_]=_
 

From aa9978c1df746b4d4f019fb7c044c2871afc64ac Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 27 Jul 2026 05:08:12 +0100
Subject: [PATCH 2/5] streamline case analysis

---
 src/Data/List/Relation/Unary/All/Properties.agda | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/Data/List/Relation/Unary/All/Properties.agda b/src/Data/List/Relation/Unary/All/Properties.agda
index e21a771eac..a31e26e36f 100644
--- a/src/Data/List/Relation/Unary/All/Properties.agda
+++ b/src/Data/List/Relation/Unary/All/Properties.agda
@@ -76,8 +76,7 @@ Null⇒null : Null xs → T (null xs)
 Null⇒null [] = _
 
 null⇒Null : T (null xs) → Null xs
-null⇒Null {xs = []   } _ = []
-null⇒Null {xs = _ ∷ _} ()
+null⇒Null {xs = []} _ = []
 
 null-∷ : Null (x ∷ xs) → Whatever
 null-∷ (() ∷ _)

From b72f05c32e464f3ab08634dde810909dd7bff597 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 31 Jul 2026 16:45:40 +0100
Subject: [PATCH 3/5] =?UTF-8?q?fix:=20regularise=20`null-=E2=88=B7`=20to?=
 =?UTF-8?q?=20use=20`=C2=AC=5F`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 CHANGELOG.md                                     | 2 +-
 src/Data/List/Relation/Unary/All/Properties.agda | 3 +--
 2 files changed, 2 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2215a2f227..89ac66f2e0 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -425,7 +425,7 @@ Additions to existing modules
 
 * In `Data.List.Relation.Unary.All.Properties`:
   ```agda
-  null-∷          : Null (x ∷ xs) → Whatever
+  null-∷          : ¬ Null (x ∷ xs)
   null?           : Decidable Null
   null-irrelevant : Irrelevant Null
   ```
diff --git a/src/Data/List/Relation/Unary/All/Properties.agda b/src/Data/List/Relation/Unary/All/Properties.agda
index a31e26e36f..f53af158ba 100644
--- a/src/Data/List/Relation/Unary/All/Properties.agda
+++ b/src/Data/List/Relation/Unary/All/Properties.agda
@@ -61,7 +61,6 @@ private
     R : Pred C r
     x y : A
     xs ys : List A
-    Whatever : Set _
 
 
 ------------------------------------------------------------------------
@@ -78,7 +77,7 @@ Null⇒null [] = _
 null⇒Null : T (null xs) → Null xs
 null⇒Null {xs = []} _ = []
 
-null-∷ : Null (x ∷ xs) → Whatever
+null-∷ : ¬ Null (x ∷ xs)
 null-∷ (() ∷ _)
 
 null? : Decidable (Null {A = A})

From 49b224fb9713211163a9f5b1f022259dcdee904e Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 3 Aug 2026 18:06:09 +0100
Subject: [PATCH 4/5] fix: capitalisation

---
 CHANGELOG.md | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 89ac66f2e0..5c42918fd3 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -425,9 +425,9 @@ Additions to existing modules
 
 * In `Data.List.Relation.Unary.All.Properties`:
   ```agda
-  null-∷          : ¬ Null (x ∷ xs)
-  null?           : Decidable Null
-  null-irrelevant : Irrelevant Null
+  ¬Null-∷         : ¬ Null (x ∷ xs)
+  Null?           : Decidable Null
+  Null-irrelevant : Irrelevant Null
   ```
 
 * In `Data.Nat.DivMod`:

From 5a96ca6e9691967f455cd112d151bbdd4feb0e9f Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 3 Aug 2026 18:07:46 +0100
Subject: [PATCH 5/5] fix: capitalisation

---
 src/Data/List/Relation/Unary/All/Properties.agda | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/Data/List/Relation/Unary/All/Properties.agda b/src/Data/List/Relation/Unary/All/Properties.agda
index f53af158ba..b8daba113c 100644
--- a/src/Data/List/Relation/Unary/All/Properties.agda
+++ b/src/Data/List/Relation/Unary/All/Properties.agda
@@ -77,15 +77,15 @@ Null⇒null [] = _
 null⇒Null : T (null xs) → Null xs
 null⇒Null {xs = []} _ = []
 
-null-∷ : ¬ Null (x ∷ xs)
-null-∷ (() ∷ _)
+¬Null-∷ : ¬ Null (x ∷ xs)
+¬Null-∷ (() ∷ _)
 
-null? : Decidable (Null {A = A})
-null? []      = yes []
-null? (_ ∷ _) = no null-∷
+Null? : Decidable (Null {A = A})
+Null? []      = yes []
+Null? (_ ∷ _) = no ¬Null-∷
 
-null-irrelevant : Irrelevant (Null {A = A})
-null-irrelevant [] [] = refl
+Null-irrelevant : Irrelevant (Null {A = A})
+Null-irrelevant [] [] = refl
 
 ------------------------------------------------------------------------
 -- Properties of the "points-to" relation _[_]=_