From 0d16e235a15ada77771a961c14e1a3554472ab07 Mon Sep 17 00:00:00 2001
From: matthewdaggitt <matthewdaggitt@gmail.com>
Date: Thu, 6 Nov 2025 23:52:25 +0800
Subject: [PATCH 1/2] Add various relations over non-empty lists

---
 CHANGELOG.md                                  | 13 +++++
 .../NonEmpty/Membership/Propositional.agda    | 27 ++++++++++
 src/Data/List/NonEmpty/Membership/Setoid.agda | 28 +++++++++++
 .../NonEmpty/Relation/Binary/Pointwise.agda   | 33 +++++++++++++
 .../List/NonEmpty/Relation/Unary/All.agda     | 15 +++++-
 .../List/NonEmpty/Relation/Unary/Any.agda     | 49 +++++++++++++++++++
 src/Data/List/Relation/Unary/Any.agda         |  2 +-
 7 files changed, 164 insertions(+), 3 deletions(-)
 create mode 100644 src/Data/List/NonEmpty/Membership/Propositional.agda
 create mode 100644 src/Data/List/NonEmpty/Membership/Setoid.agda
 create mode 100644 src/Data/List/NonEmpty/Relation/Binary/Pointwise.agda
 create mode 100644 src/Data/List/NonEmpty/Relation/Unary/Any.agda

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6679049fd0..c8598711a2 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -93,6 +93,14 @@ New modules
 
 * `Effect.Monad.Random` and `Effect.Monad.Random.Instances` for an mtl-style randomness monad constraint.
 
+* Various additions over non-empty lists:
+  ```
+  Data.List.NonEmpty.Relation.Binary.Pointwise
+  Data.List.NonEmpty.Relation.Unary.Any
+  Data.List.NonEmpty.Membership.Propositional
+  Data.List.NonEmpty.Membership.Setoid
+  ```
+
 Additions to existing modules
 -----------------------------
 
@@ -159,6 +167,11 @@ Additions to existing modules
   search-least⟨¬_⟩ : Decidable P → Π[ P ] ⊎ Least⟨ ∁ P ⟩
   ```
 
+* In `Data.List.NonEmpty.Relation.Unary.All`:
+  ```
+  map : P ⊆ Q → All P xs → All Q xs
+  ```
+
 * In `Data.Nat.ListAction.Properties`
   ```agda
   *-distribˡ-sum : ∀ m ns → m * sum ns ≡ sum (map (m *_) ns)
diff --git a/src/Data/List/NonEmpty/Membership/Propositional.agda b/src/Data/List/NonEmpty/Membership/Propositional.agda
new file mode 100644
index 0000000000..0f74ac5783
--- /dev/null
+++ b/src/Data/List/NonEmpty/Membership/Propositional.agda
@@ -0,0 +1,27 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Propositional membership over non-empty lists
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.List.NonEmpty.Membership.Propositional {a} {A : Set a} where
+
+open import Relation.Binary.PropositionalEquality using (setoid; refl)
+open import Data.List.NonEmpty
+open import Level
+open import Relation.Unary using (Pred)
+
+import Data.List.NonEmpty.Membership.Setoid as SetoidMembership
+
+private
+  variable
+    p : Level
+    P : Pred A p
+    xs : List⁺ A
+
+------------------------------------------------------------------------
+-- Re-export contents of setoid membership
+
+open SetoidMembership (setoid A) public
diff --git a/src/Data/List/NonEmpty/Membership/Setoid.agda b/src/Data/List/NonEmpty/Membership/Setoid.agda
new file mode 100644
index 0000000000..815146c352
--- /dev/null
+++ b/src/Data/List/NonEmpty/Membership/Setoid.agda
@@ -0,0 +1,28 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Setoid membership over non-empty lists
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Relation.Binary.Bundles using (Setoid)
+
+module Data.List.NonEmpty.Membership.Setoid {c ℓ} (S : Setoid c ℓ) where
+
+open import Data.List.NonEmpty.Base using (List⁺)
+open import Data.List.NonEmpty.Relation.Unary.Any using (Any)
+open import Relation.Nullary.Negation using (¬_)
+
+open Setoid S renaming (Carrier to A)
+
+------------------------------------------------------------------------
+-- Definitions
+
+infix 4 _∈_ _∉_
+
+_∈_ : A → List⁺ A → Set _
+x ∈ xs = Any (x ≈_) xs
+
+_∉_ : A → List⁺ A → Set _
+x ∉ xs = ¬ x ∈ xs
diff --git a/src/Data/List/NonEmpty/Relation/Binary/Pointwise.agda b/src/Data/List/NonEmpty/Relation/Binary/Pointwise.agda
new file mode 100644
index 0000000000..0ae4b57786
--- /dev/null
+++ b/src/Data/List/NonEmpty/Relation/Binary/Pointwise.agda
@@ -0,0 +1,33 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Pointwise lifting of relations to non-empty lists
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.List.NonEmpty.Relation.Binary.Pointwise where
+
+open import Data.List.Base using (List; []; _∷_)
+open import Data.List.NonEmpty.Base using (List⁺; _∷_)
+import Data.List.Relation.Binary.Pointwise.Base as List
+open import Level
+open import Relation.Binary.Core using (REL)
+
+private
+  variable
+    a b ℓ : Level
+    A B : Set a
+    x y : A
+    xs ys : List A
+
+------------------------------------------------------------------------
+-- Definition
+------------------------------------------------------------------------
+
+infixr 5 _∷_
+
+data Pointwise {A : Set a} {B : Set b} (R : REL A B ℓ)
+               : List⁺ A → List⁺ B → Set (a ⊔ b ⊔ ℓ) where
+  _∷_ : (x∼y : R x y) (xs∼ys : List.Pointwise R xs ys) →
+         Pointwise R (x ∷ xs) (y ∷ ys)
diff --git a/src/Data/List/NonEmpty/Relation/Unary/All.agda b/src/Data/List/NonEmpty/Relation/Unary/All.agda
index 38fed028d1..67a8e2d4e1 100644
--- a/src/Data/List/NonEmpty/Relation/Unary/All.agda
+++ b/src/Data/List/NonEmpty/Relation/Unary/All.agda
@@ -12,14 +12,18 @@ import Data.List.Relation.Unary.All as List
 open import Data.List.Relation.Unary.All using ([]; _∷_)
 open import Data.List.Base using ([]; _∷_)
 open import Data.List.NonEmpty.Base using (List⁺; _∷_; toList)
+open import Data.List.NonEmpty.Membership.Propositional using (_∈_)
+open import Data.List.NonEmpty.Relation.Unary.Any using (here; there)
 open import Level using (Level; _⊔_)
-open import Relation.Unary using (Pred)
+open import Relation.Unary using (Pred; _⊆_)
+open import Relation.Binary.PropositionalEquality.Core using (refl)
 
 private
   variable
     a p : Level
     A : Set a
-    P : Pred A p
+    P Q : Pred A p
+    xs : List⁺ A
 
 ------------------------------------------------------------------------
 -- Definition
@@ -35,5 +39,12 @@ data All {A : Set a} (P : Pred A p) : Pred (List⁺ A) (a ⊔ p) where
 ------------------------------------------------------------------------
 -- Functions
 
+map : P ⊆ Q → All P xs → All Q xs
+map P⊆Q (px ∷ pxs) = P⊆Q px ∷ List.map P⊆Q pxs
+
+lookup : All P xs → ∀ {x} → x ∈ xs → P x
+lookup (px ∷ pxs) (here refl)   = px
+lookup (px ∷ pxs) (there x∈xs) = List.lookup pxs x∈xs
+
 toList⁺ : ∀ {xs : List⁺ A} → All P xs → List.All P (toList xs)
 toList⁺ (px ∷ pxs) = px ∷ pxs
diff --git a/src/Data/List/NonEmpty/Relation/Unary/Any.agda b/src/Data/List/NonEmpty/Relation/Unary/Any.agda
new file mode 100644
index 0000000000..4f4d0cc5ac
--- /dev/null
+++ b/src/Data/List/NonEmpty/Relation/Unary/Any.agda
@@ -0,0 +1,49 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Non-empty lists where at least one element satisfies a given property
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.List.NonEmpty.Relation.Unary.Any where
+
+open import Data.List.NonEmpty using (List⁺; _∷_)
+
+open import Data.List.Relation.Unary.Any as List using (here; there)
+open import Data.List.Base using ([]; _∷_)
+open import Data.List.NonEmpty.Base using (List⁺; _∷_; toList)
+open import Data.Product.Base using (_,_)
+open import Level using (Level; _⊔_)
+open import Relation.Unary using (Pred; Satisfiable; _⊆_)
+
+private
+  variable
+    a p : Level
+    A : Set a
+    P Q : Pred A p
+    xs : List⁺ A
+
+------------------------------------------------------------------------
+-- Definition
+
+-- Given a predicate P, then Any P xs means that every element in xs
+-- satisfies P. See `Relation.Unary` for an explanation of predicates.
+
+data Any {A : Set a} (P : Pred A p) : Pred (List⁺ A) (a ⊔ p) where
+  here : ∀ {x xs} (px : P x) → Any P (x ∷ xs)
+  there : ∀ {x xs} (pxs : List.Any P xs) → Any P (x ∷ xs)
+
+------------------------------------------------------------------------
+-- Operations
+
+map : P ⊆ Q → Any P ⊆ Any Q
+map g (here px)   = here (g px)
+map g (there pxs) = there (List.map g pxs)
+
+------------------------------------------------------------------------
+-- Predicates
+
+satisfied : Any P xs → Satisfiable P
+satisfied (here px)  = _ , px
+satisfied (there pxs) = List.satisfied pxs
diff --git a/src/Data/List/Relation/Unary/Any.agda b/src/Data/List/Relation/Unary/Any.agda
index b43a84bb7b..f5500a5261 100644
--- a/src/Data/List/Relation/Unary/Any.agda
+++ b/src/Data/List/Relation/Unary/Any.agda
@@ -71,7 +71,7 @@ xs ─ x∈xs = removeAt xs (index x∈xs)
 
 -- If any element satisfies P, then P is satisfied.
 
-satisfied : Any P xs → ∃ P
+satisfied : Any P xs → Satisfiable P
 satisfied (here px)   = _ , px
 satisfied (there pxs) = satisfied pxs
 

From b093e75fa3bedce871b2bbd3e0ceae15ae4a89a7 Mon Sep 17 00:00:00 2001
From: matthewdaggitt <matthewdaggitt@gmail.com>
Date: Sat, 8 Nov 2025 10:44:50 +0800
Subject: [PATCH 2/2] Address James' feedback

---
 src/Data/List/NonEmpty/Relation/Unary/All.agda | 2 +-
 src/Data/List/NonEmpty/Relation/Unary/Any.agda | 4 +---
 2 files changed, 2 insertions(+), 4 deletions(-)

diff --git a/src/Data/List/NonEmpty/Relation/Unary/All.agda b/src/Data/List/NonEmpty/Relation/Unary/All.agda
index 67a8e2d4e1..72c7abcace 100644
--- a/src/Data/List/NonEmpty/Relation/Unary/All.agda
+++ b/src/Data/List/NonEmpty/Relation/Unary/All.agda
@@ -39,7 +39,7 @@ data All {A : Set a} (P : Pred A p) : Pred (List⁺ A) (a ⊔ p) where
 ------------------------------------------------------------------------
 -- Functions
 
-map : P ⊆ Q → All P xs → All Q xs
+map : P ⊆ Q → All P ⊆ All Q
 map P⊆Q (px ∷ pxs) = P⊆Q px ∷ List.map P⊆Q pxs
 
 lookup : All P xs → ∀ {x} → x ∈ xs → P x
diff --git a/src/Data/List/NonEmpty/Relation/Unary/Any.agda b/src/Data/List/NonEmpty/Relation/Unary/Any.agda
index 4f4d0cc5ac..62a5906480 100644
--- a/src/Data/List/NonEmpty/Relation/Unary/Any.agda
+++ b/src/Data/List/NonEmpty/Relation/Unary/Any.agda
@@ -8,11 +8,9 @@
 
 module Data.List.NonEmpty.Relation.Unary.Any where
 
-open import Data.List.NonEmpty using (List⁺; _∷_)
-
+open import Data.List.NonEmpty.Base using (List⁺; _∷_; toList)
 open import Data.List.Relation.Unary.Any as List using (here; there)
 open import Data.List.Base using ([]; _∷_)
-open import Data.List.NonEmpty.Base using (List⁺; _∷_; toList)
 open import Data.Product.Base using (_,_)
 open import Level using (Level; _⊔_)
 open import Relation.Unary using (Pred; Satisfiable; _⊆_)