From d54c553fca424f3a2fc88ef22f4372bc49214852 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 2 May 2024 06:00:06 +0100
Subject: [PATCH 1/3] fixes #2375

---
 CHANGELOG.md                                  |  5 ++++
 .../Binary/Subset/Setoid/Properties.agda      | 26 +++++++++++++++++--
 2 files changed, 29 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 895a3ad3bd..bdc6da609b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -373,6 +373,11 @@ Additions to existing modules
   map-catMaybes         : map f ∘ catMaybes ≗ catMaybes ∘ map (Maybe.map f)
   ```
 
+* In `Data.List.Relation.Binary.Subset.Setoid.Properties`
+  ```
+  map⁺ : f Preserves _≈_ ⟶ _≈′_ → as ⊆ bs → map f as ⊆′ map f bs
+  ```
+
 * In `Data.List.Relation.Unary.All.Properties`:
   ```agda
   All-catMaybes⁺ : All (Maybe.All P) xs → All P (catMaybes xs)
diff --git a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda
index bc1a693a2f..a867d31fba 100644
--- a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda
@@ -26,7 +26,7 @@ open import Level using (Level)
 open import Relation.Nullary using (¬_; does; yes; no)
 open import Relation.Nullary.Negation using (contradiction)
 open import Relation.Unary using (Pred; Decidable) renaming (_⊆_ to _⋐_)
-open import Relation.Binary.Core using (_⇒_)
+open import Relation.Binary.Core using (_⇒_; _Preserves_⟶_)
 open import Relation.Binary.Definitions
   using (Reflexive; Transitive; _Respectsʳ_; _Respectsˡ_; _Respects_)
 open import Relation.Binary.Bundles using (Setoid; Preorder)
@@ -38,7 +38,7 @@ open Setoid using (Carrier)
 
 private
   variable
-    a p q ℓ : Level
+    a b p q r ℓ : Level
 
 ------------------------------------------------------------------------
 -- Relational properties with _≋_ (pointwise equality)
@@ -206,6 +206,28 @@ module _ (S : Setoid a ℓ) where
   ++⁺ : ∀ {ws xs ys zs} → ws ⊆ xs → ys ⊆ zs → ws ++ ys ⊆ xs ++ zs
   ++⁺ ws⊆xs ys⊆zs = ⊆-trans S (++⁺ˡ _ ws⊆xs) (++⁺ʳ _ ys⊆zs)
 
+------------------------------------------------------------------------
+-- map
+
+module _ (S : Setoid a ℓ) (R : Setoid b r) where
+
+  private
+    module S = Setoid S
+    module R = Setoid R
+
+    module S∈ = Membership S
+    module R∈ = Membership R
+
+    module S⊆ = Subset S
+    module R⊆ = Subset R
+
+  map⁺ : ∀ {as bs} {f : S.Carrier → R.Carrier} →
+         f Preserves S._≈_ ⟶ R._≈_ →
+         as S⊆.⊆ bs → map f as R⊆.⊆ map f bs
+  map⁺ {f = f} f-pres as⊆bs v∈f[as] =
+    let x , x∈as , v≈f[x] = ∈-map⁻ S R v∈f[as] in
+    ∈-resp-≈ R (R.sym v≈f[x]) (∈-map⁺ S R f-pres (as⊆bs x∈as))
+
 ------------------------------------------------------------------------
 -- filter
 

From ca5a1f4b4e94bd9ce8804d267c2e793d438c9db8 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 2 May 2024 12:57:51 +0100
Subject: [PATCH 2/3] removed redundant `Membership` instances

---
 src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda
index a867d31fba..e4b8690bce 100644
--- a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda
@@ -215,9 +215,6 @@ module _ (S : Setoid a ℓ) (R : Setoid b r) where
     module S = Setoid S
     module R = Setoid R
 
-    module S∈ = Membership S
-    module R∈ = Membership R
-
     module S⊆ = Subset S
     module R⊆ = Subset R
 

From 915c8e74f6339f02e1eba3b17b2f798295ee5515 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 14 May 2024 13:13:34 +0100
Subject: [PATCH 3/3] fix merge conflict error

---
 src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda
index 4e9233e970..0d0d685a27 100644
--- a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda
@@ -222,6 +222,8 @@ module _ (S : Setoid a ℓ) (R : Setoid b r) where
     module S⊆ = Subset S
     module R⊆ = Subset R
 
+  open Membershipₚ
+
   map⁺ : ∀ {as bs} {f : S.Carrier → R.Carrier} →
          f Preserves S._≈_ ⟶ R._≈_ →
          as S⊆.⊆ bs → map f as R⊆.⊆ map f bs