From 8315f5cbf4e759df15a1c0d6e7cca0b8994ec741 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Wed, 20 Mar 2024 21:05:57 +0000
Subject: [PATCH 01/47] =?UTF-8?q?`contradiction`=20against=20`=E2=8A=A5-el?=
 =?UTF-8?q?im`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

diff --git a/src/Data/List/Relation/Unary/Any.agda b/src/Data/List/Relation/Unary/Any.agda
index 1b6093cadc..d80043b575 100644
--- a/src/Data/List/Relation/Unary/Any.agda
+++ b/src/Data/List/Relation/Unary/Any.agda
@@ -8,7 +8,6 @@
 
 module Data.List.Relation.Unary.Any where
 
-open import Data.Empty
 open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.List.Base as List using (List; []; [_]; _∷_; removeAt)
 open import Data.Product.Base as Product using (∃; _,_)
@@ -46,7 +45,7 @@ head ¬pxs (here px)   = px
 head ¬pxs (there pxs) = contradiction pxs ¬pxs
 
 tail : ¬ P x → Any P (x ∷ xs) → Any P xs
-tail ¬px (here  px)  = ⊥-elim (¬px px)
+tail ¬px (here  px)  = contradiction px ¬px
 tail ¬px (there pxs) = pxs
 
 map : P ⊆ Q → Any P ⊆ Any Q

From 2f3893c76c120a6d48bd272027a4f2c3bc5abbb3 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 21 Mar 2024 07:46:54 +0000
Subject: [PATCH 02/47] tightened `import`s

---
 src/Data/List/Relation/Unary/Any.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/List/Relation/Unary/Any.agda b/src/Data/List/Relation/Unary/Any.agda
index d80043b575..ad9707cd77 100644
--- a/src/Data/List/Relation/Unary/Any.agda
+++ b/src/Data/List/Relation/Unary/Any.agda
@@ -16,7 +16,7 @@ open import Level using (Level; _⊔_)
 open import Relation.Nullary using (¬_; yes; no; _⊎-dec_)
 import Relation.Nullary.Decidable as Dec
 open import Relation.Nullary.Negation using (contradiction)
-open import Relation.Unary hiding (_∈_)
+open import Relation.Unary using (Pred; _⊆_; Decidable; Satisfiable)
 
 private
   variable

From 1eab803bdf3ca0149dc14bcba4893b985fdeafa1 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 21 Mar 2024 07:47:53 +0000
Subject: [PATCH 03/47] =?UTF-8?q?added=20two=20operations=20`=E2=88=83?=
 =?UTF-8?q?=E2=88=88`=20and=20`=E2=88=80=E2=88=88`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Data/List/Membership/Setoid.agda | 17 ++++++++++++-----
 1 file changed, 12 insertions(+), 5 deletions(-)

diff --git a/src/Data/List/Membership/Setoid.agda b/src/Data/List/Membership/Setoid.agda
index cadc600646..9c6052309a 100644
--- a/src/Data/List/Membership/Setoid.agda
+++ b/src/Data/List/Membership/Setoid.agda
@@ -9,9 +9,9 @@
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Definitions using (_Respects_)
 
-module Data.List.Membership.Setoid {c ℓ} (S : Setoid c ℓ) where
+module Data.List.Membership.SetoidNEW {c ℓ} (S : Setoid c ℓ) where
 
-open import Function.Base using (_∘_; id; flip)
+open import Function.Base using (_∘_; id; flip; const)
 open import Data.List.Base as List using (List; []; _∷_; length; lookup)
 open import Data.List.Relation.Unary.Any as Any
   using (Any; index; map; here; there)
@@ -32,6 +32,12 @@ x ∈ xs = Any (x ≈_) xs
 _∉_ : A → List A → Set _
 x ∉ xs = ¬ x ∈ xs
 
+∃∈ : ∀ {p} (P : Pred A p) → Pred (List A) _
+∃∈ P xs = ∃ λ x → x ∈ xs × P x
+
+∀∈ : ∀ {p} (P : Pred A p) → Pred (List A) _
+∀∈ P xs = ∀ {x} → x ∈ xs → P x
+
 ------------------------------------------------------------------------
 -- Operations
 
@@ -39,7 +45,7 @@ _∷=_ = Any._∷=_ {A = A}
 _─_ = Any._─_ {A = A}
 
 mapWith∈ : ∀ {b} {B : Set b}
-           (xs : List A) → (∀ {x} → x ∈ xs → B) → List B
+           (xs : List A) → (∀∈ (const B) xs) → List B
 mapWith∈ []       f = []
 mapWith∈ (x ∷ xs) f = f (here refl) ∷ mapWith∈ xs (f ∘ there)
 
@@ -48,9 +54,10 @@ mapWith∈ (x ∷ xs) f = f (here refl) ∷ mapWith∈ xs (f ∘ there)
 
 module _ {p} {P : Pred A p} where
 
-  find : ∀ {xs} → Any P xs → ∃ λ x → x ∈ xs × P x
-  find (here px)   = (_ , here refl , px)
+  find : ∀ {xs} → Any P xs → ∃∈ P xs
+  find (here px)   = _ , here refl , px
   find (there pxs) = Product.map id (Product.map there id) (find pxs)
+  -- let x , x∈xs , px = find pxs in x , there x∈xs , px
 
   lose : P Respects _≈_ →  ∀ {x xs} → x ∈ xs → P x → Any P xs
   lose resp x∈xs px = map (flip resp px) x∈xs

From 4f8b36fb14f735f91215a260b47609bb03ea4173 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 21 Mar 2024 08:11:07 +0000
Subject: [PATCH 04/47] added to `CHANGELOG`

---
 CHANGELOG.md                         | 16 +++++++++++-----
 src/Data/List/Membership/Setoid.agda |  2 +-
 2 files changed, 12 insertions(+), 6 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 1cb95ff90b..2109669a0e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -170,7 +170,7 @@ Additions to existing modules
   quasigroup      : Quasigroup _ _
   isLoop          : IsLoop _∙_ _\\_ _//_ ε
   loop            : Loop _ _
-  
+
   \\-leftDividesˡ  : LeftDividesˡ _∙_ _\\_
   \\-leftDividesʳ  : LeftDividesʳ _∙_ _\\_
   \\-leftDivides   : LeftDivides _∙_ _\\_
@@ -189,7 +189,7 @@ Additions to existing modules
   identityʳ-unique : x ∙ y ≈ x → y ≈ ε
   identity-unique  : Identity x _∙_ → x ≈ ε
   ```
- 
+
 * In `Algebra.Construct.Terminal`:
   ```agda
   rawNearSemiring : RawNearSemiring c ℓ
@@ -218,7 +218,7 @@ Additions to existing modules
   _\\_ : Op₂ A
   x \\ y = (x ⁻¹) ∙ y
   ```
- 
+
 * In `Data.Container.Indexed.Core`:
   ```agda
   Subtrees o c = (r : Response c) → X (next c r)
@@ -229,11 +229,17 @@ Additions to existing modules
   nonZeroIndex : Fin n → ℕ.NonZero n
   ```
 
-* In `Data.Integer.Divisisbility`: introduce `divides` as an explicit pattern synonym
+* In `Data.Integer.Divisibility`: introduce `divides` as an explicit pattern synonym
   ```agda
   pattern divides k eq = Data.Nat.Divisibility.divides k eq
   ```
 
+* In `Data.List.Membership.Setoid`: two abbreviations for predicate transformers
+  ```agda
+  ∃∈ P xs = ∃ λ x → x ∈ xs × P x
+  ∀∈ P xs = ∀ {x} → x ∈ xs → P x
+  ```
+
 * In `Data.List.Properties`:
   ```agda
   applyUpTo-∷ʳ          : applyUpTo f n ∷ʳ f n ≡ applyUpTo f (suc n)
@@ -320,7 +326,7 @@ Additions to existing modules
   pred-injective : .{{NonZero m}} → .{{NonZero n}} → pred m ≡ pred n → m ≡ n
   pred-cancel-≡ : pred m ≡ pred n → ((m ≡ 0 × n ≡ 1) ⊎ (m ≡ 1 × n ≡ 0)) ⊎ m ≡ n
   ```
-  
+
 * Added new proofs to `Data.Nat.Primality`:
   ```agda
   rough∧square>⇒prime : .{{NonTrivial n}} → m Rough n → m * m > n → Prime n
diff --git a/src/Data/List/Membership/Setoid.agda b/src/Data/List/Membership/Setoid.agda
index 9c6052309a..9919bf9409 100644
--- a/src/Data/List/Membership/Setoid.agda
+++ b/src/Data/List/Membership/Setoid.agda
@@ -9,7 +9,7 @@
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Definitions using (_Respects_)
 
-module Data.List.Membership.SetoidNEW {c ℓ} (S : Setoid c ℓ) where
+module Data.List.Membership.Setoid {c ℓ} (S : Setoid c ℓ) where
 
 open import Function.Base using (_∘_; id; flip; const)
 open import Data.List.Base as List using (List; []; _∷_; length; lookup)

From f1348abe835887a0608ce662da0e0c9e414b1dd5 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 21 Mar 2024 08:12:21 +0000
Subject: [PATCH 05/47] knock-on for the `Propositional` case

---
 src/Data/List/Membership/Propositional.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Data/List/Membership/Propositional.agda b/src/Data/List/Membership/Propositional.agda
index c1ae08761e..2f5edc2d7e 100644
--- a/src/Data/List/Membership/Propositional.agda
+++ b/src/Data/List/Membership/Propositional.agda
@@ -10,7 +10,7 @@
 module Data.List.Membership.Propositional {a} {A : Set a} where
 
 open import Data.List.Relation.Unary.Any using (Any)
-open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; subst)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; resp; subst)
 open import Relation.Binary.PropositionalEquality.Properties using (setoid)
 
 import Data.List.Membership.Setoid as SetoidMembership
@@ -32,4 +32,4 @@ _≢∈_ x∈xs y∈xs = ∀ x≡y → subst (_∈ _) x≡y x∈xs ≢ y∈xs
 -- Other operations
 
 lose : ∀ {p} {P : A → Set p} {x xs} → x ∈ xs → P x → Any P xs
-lose = SetoidMembership.lose (setoid A) (subst _)
+lose = SetoidMembership.lose (setoid A) (resp _)

From e09c7287f7ae9399526d57d65eca4a1d453ddb6e Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 21 Mar 2024 08:34:42 +0000
Subject: [PATCH 06/47] =?UTF-8?q?refactor=20`lose=E2=88=98find`=20and=20`f?=
 =?UTF-8?q?ind=E2=88=98lose`=20in=20terms=20of=20new=20lemmas=20`=E2=88=83?=
 =?UTF-8?q?=E2=88=88-Any=E2=88=98find`=20and=20`find=E2=88=98=E2=88=83?=
 =?UTF-8?q?=E2=88=88-Any`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .../Propositional/Properties/Core.agda        | 84 +++++++++----------
 1 file changed, 41 insertions(+), 43 deletions(-)

diff --git a/src/Data/List/Membership/Propositional/Properties/Core.agda b/src/Data/List/Membership/Propositional/Properties/Core.agda
index ca8ffbb1ea..df3210672a 100644
--- a/src/Data/List/Membership/Propositional/Properties/Core.agda
+++ b/src/Data/List/Membership/Propositional/Properties/Core.agda
@@ -12,75 +12,73 @@
 
 module Data.List.Membership.Propositional.Properties.Core where
 
-open import Function.Base using (flip; id; _∘_)
-open import Function.Bundles
 open import Data.List.Base using (List)
 open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
 open import Data.List.Membership.Propositional
-open import Data.Product.Base as Product
-  using (_,_; proj₁; proj₂; uncurry′; ∃; _×_)
+open import Data.Product.Base as Product using (_,_)
+open import Function.Base using (flip; id; _∘_)
+open import Function.Bundles using (_↔_; mk↔ₛ′)
 open import Level using (Level)
 open import Relation.Binary.PropositionalEquality.Core
-  using (_≡_; refl; cong; subst)
+  using (_≡_; refl; cong; resp)
 open import Relation.Unary using (Pred; _⊆_)
 
 private
   variable
     a p q : Level
     A : Set a
-
-------------------------------------------------------------------------
--- Lemmas relating map and find.
-
-map∘find : ∀ {P : Pred A p} {xs}
-           (p : Any P xs) → let p′ = find p in
-           {f : _≡_ (proj₁ p′) ⊆ P} →
-           f refl ≡ proj₂ (proj₂ p′) →
-           Any.map f (proj₁ (proj₂ p′)) ≡ p
-map∘find (here  p) hyp = cong here  hyp
-map∘find (there p) hyp = cong there (map∘find p hyp)
-
-find∘map : ∀ {P : Pred A p} {Q : Pred A q}
-           {xs : List A} (p : Any P xs) (f : P ⊆ Q) →
-           find (Any.map f p) ≡ Product.map id (Product.map id f) (find p)
-find∘map (here  p) f = refl
-find∘map (there p) f rewrite find∘map p f = refl
+    x : A
+    xs : List A
 
 ------------------------------------------------------------------------
 -- find satisfies a simple equality when the predicate is a
 -- propositional equality.
 
-find-∈ : ∀ {x : A} {xs : List A} (x∈xs : x ∈ xs) →
-         find x∈xs ≡ (x , x∈xs , refl)
+find-∈ : (x∈xs : x ∈ xs) → find x∈xs ≡ (x , x∈xs , refl)
 find-∈ (here refl)  = refl
 find-∈ (there x∈xs) rewrite find-∈ x∈xs = refl
 
 ------------------------------------------------------------------------
--- find and lose are inverses (more or less).
+-- Lemmas relating map and find.
+
+module _ {P : Pred A p} where
 
-lose∘find : ∀ {P : Pred A p} {xs : List A}
-            (p : Any P xs) →
-            uncurry′ lose (proj₂ (find p)) ≡ p
-lose∘find p = map∘find p refl
+  map∘find : (p : Any P xs) → let x , x∈xs , px = find p in
+             {f : (x ≡_) ⊆ P} → f refl ≡ px →
+             Any.map f x∈xs ≡ p
+  map∘find (here  p) hyp = cong here  hyp
+  map∘find (there p) hyp = cong there (map∘find p hyp)
 
-find∘lose : ∀ (P : Pred A p) {x xs}
-            (x∈xs : x ∈ xs) (pp : P x) →
-            find {P = P} (lose x∈xs pp) ≡ (x , x∈xs , pp)
-find∘lose P x∈xs p
-  rewrite find∘map x∈xs (flip (subst P) p)
-        | find-∈ x∈xs
-        = refl
+  find∘map : ∀ {Q : Pred A q} {xs} (p : Any P xs) (f : P ⊆ Q) →
+             find (Any.map f p) ≡ Product.map id (Product.map id f) (find p)
+  find∘map (here  p) f = refl
+  find∘map (there p) f rewrite find∘map p f = refl
 
 ------------------------------------------------------------------------
 -- Any can be expressed using _∈_
 
 module _ {P : Pred A p} where
 
-  ∃∈-Any : ∀  {xs} → (∃ λ x → x ∈ xs × P x) → Any P xs
-  ∃∈-Any = uncurry′ lose ∘ proj₂
+  ∃∈-Any : ∃∈ P xs → Any P xs
+  ∃∈-Any (x , x∈xs , px) = lose {P = P} x∈xs px
+
+  find∘∃∈-Any : (p : ∃∈ P xs) → find (∃∈-Any p) ≡ p
+  find∘∃∈-Any p@(x , x∈xs , px)
+    rewrite find∘map x∈xs (flip (resp P) px) | find-∈ x∈xs = refl
+
+  ∃∈-Any∘find : (p : Any P xs) → ∃∈-Any (find p) ≡ p
+  ∃∈-Any∘find p = map∘find p refl
+
+  Any↔ : ∃∈ P xs ↔ Any P xs
+  Any↔ = mk↔ₛ′ ∃∈-Any find ∃∈-Any∘find find∘∃∈-Any
 
-  Any↔ : ∀ {xs} → (∃ λ x → x ∈ xs × P x) ↔ Any P xs
-  Any↔ = mk↔ₛ′ ∃∈-Any find lose∘find from∘to
-    where
-    from∘to : ∀ v → find (∃∈-Any v) ≡ v
-    from∘to p = find∘lose _ (proj₁ (proj₂ p)) (proj₂ (proj₂ p))
+------------------------------------------------------------------------
+-- Hence, find and lose are inverses (more or less).
+
+lose∘find : ∀ {P : Pred A p} {xs} (p : Any P xs) → ∃∈-Any (find p) ≡ p
+lose∘find = ∃∈-Any∘find
+
+find∘lose : ∀ (P : Pred A p) {x xs}
+            (x∈xs : x ∈ xs) (px : P x) →
+            find (lose {P = P} x∈xs px) ≡ (x , x∈xs , px)
+find∘lose P {x} x∈xs px = find∘∃∈-Any (x , x∈xs , px)

From 7710d1065a9bb35c97b3ab5b63b5fdce38009519 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 21 Mar 2024 08:36:04 +0000
Subject: [PATCH 07/47] `CHANGELOG`

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2109669a0e..eec3f40cab 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -234,6 +234,12 @@ Additions to existing modules
   pattern divides k eq = Data.Nat.Divisibility.divides k eq
   ```
 
+* In `Data.List.Membership.Propositional.Properties.Core`:
+  ```agda
+  find∘∃∈-Any : (p : ∃∈ P xs) → find (∃∈-Any p) ≡ p
+  ∃∈-Any∘find : (p : Any P xs) → ∃∈-Any (find p) ≡ p
+  ```
+
 * In `Data.List.Membership.Setoid`: two abbreviations for predicate transformers
   ```agda
   ∃∈ P xs = ∃ λ x → x ∈ xs × P x
@@ -252,6 +258,11 @@ Additions to existing modules
   reverse-downFrom      : reverse (downFrom n) ≡ upTo n
   ```
 
+* In `Data.List.Relation.Unary.All`:
+  ```agda
+  universal-U : Universal (All U)
+  ```
+
 * In `Data.List.Relation.Unary.All.Properties`:
   ```agda
   All-catMaybes⁺ : All (Maybe.All P) xs → All P (catMaybes xs)

From d5a4cd94c0abf5ab37f3d8b4f10e734e83b24c75 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 21 Mar 2024 08:37:52 +0000
Subject: [PATCH 08/47] reorder

---
 src/Data/List/Membership/Propositional/Properties/Core.agda | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Data/List/Membership/Propositional/Properties/Core.agda b/src/Data/List/Membership/Propositional/Properties/Core.agda
index df3210672a..27a29081cd 100644
--- a/src/Data/List/Membership/Propositional/Properties/Core.agda
+++ b/src/Data/List/Membership/Propositional/Properties/Core.agda
@@ -62,13 +62,13 @@ module _ {P : Pred A p} where
   ∃∈-Any : ∃∈ P xs → Any P xs
   ∃∈-Any (x , x∈xs , px) = lose {P = P} x∈xs px
 
+  ∃∈-Any∘find : (p : Any P xs) → ∃∈-Any (find p) ≡ p
+  ∃∈-Any∘find p = map∘find p refl
+
   find∘∃∈-Any : (p : ∃∈ P xs) → find (∃∈-Any p) ≡ p
   find∘∃∈-Any p@(x , x∈xs , px)
     rewrite find∘map x∈xs (flip (resp P) px) | find-∈ x∈xs = refl
 
-  ∃∈-Any∘find : (p : Any P xs) → ∃∈-Any (find p) ≡ p
-  ∃∈-Any∘find p = map∘find p refl
-
   Any↔ : ∃∈ P xs ↔ Any P xs
   Any↔ = mk↔ₛ′ ∃∈-Any find ∃∈-Any∘find find∘∃∈-Any
 

From e77363aeeb250114a37f6791ee0a0e96d360d82b Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 21 Mar 2024 08:38:22 +0000
Subject: [PATCH 09/47] knock-on viscosity

---
 src/Data/List/Relation/Unary/All.agda | 28 +++++++++++++++------------
 1 file changed, 16 insertions(+), 12 deletions(-)

diff --git a/src/Data/List/Relation/Unary/All.agda b/src/Data/List/Relation/Unary/All.agda
index bd8677630b..3c6cfa0b49 100644
--- a/src/Data/List/Relation/Unary/All.agda
+++ b/src/Data/List/Relation/Unary/All.agda
@@ -13,7 +13,7 @@ open import Effect.Monad
 open import Data.Empty using (⊥)
 open import Data.List.Base as List using (List; []; _∷_)
 open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
-open import Data.List.Membership.Propositional renaming (_∈_ to _∈ₚ_)
+open import Data.List.Membership.Propositional renaming (_∈_ to _∈ₚ_; ∀∈ to ∀∈ₚ)
 import Data.List.Membership.Setoid as SetoidMembership
 open import Data.Product.Base as Product
   using (∃; -,_; _×_; _,_; proj₁; proj₂; uncurry)
@@ -23,6 +23,7 @@ open import Level using (Level; _⊔_)
 open import Relation.Nullary hiding (Irrelevant)
 import Relation.Nullary.Decidable as Dec
 open import Relation.Unary hiding (_∈_)
+import Relation.Unary.Properties as Unary
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Definitions using (_Respects_)
 open import Relation.Binary.PropositionalEquality.Core as ≡
@@ -68,7 +69,7 @@ data _[_]=_ {A : Set a} {P : Pred A p} :
 -- A list is empty if having an element is impossible.
 
 Null : Pred (List A) _
-Null = All (λ _ → ⊥)
+Null = All ∅
 
 ------------------------------------------------------------------------
 -- Operations on All
@@ -116,17 +117,17 @@ unzip : All (P ∩ Q) ⊆ All P ∩ All Q
 unzip = unzipWith id
 
 module _(S : Setoid a ℓ) {P : Pred (Setoid.Carrier S) p} where
-  open Setoid S renaming (Carrier to C; refl to refl₁)
+  open Setoid S renaming (refl to ≈-refl)
   open SetoidMembership S
 
-  tabulateₛ : (∀ {x} → x ∈ xs → P x) → All P xs
-  tabulateₛ {[]}     hyp = []
-  tabulateₛ {x ∷ xs} hyp = hyp (here refl₁) ∷ tabulateₛ (hyp ∘ there)
+  tabulateₛ : ∀∈ P xs → All P xs
+  tabulateₛ {[]}    hyp = []
+  tabulateₛ {_ ∷ _} hyp = hyp (here ≈-refl) ∷ tabulateₛ (hyp ∘ there)
 
-tabulate : (∀ {x} → x ∈ₚ xs → P x) → All P xs
+tabulate : ∀∈ₚ P xs → All P xs
 tabulate = tabulateₛ (≡.setoid _)
 
-self : ∀ {xs : List A} → All (const A) xs
+self : ∀ {xs} → All (const A) xs
 self = tabulate (λ {x} _ → x)
 
 ------------------------------------------------------------------------
@@ -191,15 +192,15 @@ lookupAny (px ∷ pxs) (there i) = lookupAny pxs i
 lookupWith : ∀[ P ⇒ Q ⇒ R ] → All P xs → (i : Any Q xs) → R (Any.lookup i)
 lookupWith f pxs i = Product.uncurry f (lookupAny pxs i)
 
-lookup : All P xs → (∀ {x} → x ∈ₚ xs → P x)
+lookup : All P xs → ∀∈ₚ P xs
 lookup pxs = lookupWith (λ { px refl → px }) pxs
 
 module _(S : Setoid a ℓ) {P : Pred (Setoid.Carrier S) p} where
-  open Setoid S renaming (sym to sym₁)
+  open Setoid S renaming (sym to ≈-sym)
   open SetoidMembership S
 
-  lookupₛ : P Respects _≈_ → All P xs → (∀ {x} → x ∈ xs → P x)
-  lookupₛ resp pxs = lookupWith (λ py x=y → resp (sym₁ x=y) py) pxs
+  lookupₛ : P Respects _≈_ → All P xs → ∀∈ P xs
+  lookupₛ resp pxs = lookupWith (λ py x≈y → resp (≈-sym x≈y) py) pxs
 
 ------------------------------------------------------------------------
 -- Properties of predicates preserved by All
@@ -212,6 +213,9 @@ universal : Universal P → Universal (All P)
 universal u []       = []
 universal u (x ∷ xs) = u x ∷ universal u xs
 
+universal-U : Universal (All (U {A = A}))
+universal-U = universal Unary.U-Universal
+
 irrelevant : Irrelevant P → Irrelevant (All P)
 irrelevant irr []           []           = ≡.refl
 irrelevant irr (px₁ ∷ pxs₁) (px₂ ∷ pxs₂) =

From 03b33b8ec2ad3da0086e2a49793ffa897c065c88 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 21 Mar 2024 08:56:47 +0000
Subject: [PATCH 10/47] =?UTF-8?q?knock-on=20viscosity;=20plus=20refactorin?=
 =?UTF-8?q?g=20of=20`=C3=97=E2=86=94`=20for=20intelligibility?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .../List/Relation/Unary/Any/Properties.agda   | 137 +++++++++++-------
 1 file changed, 81 insertions(+), 56 deletions(-)

diff --git a/src/Data/List/Relation/Unary/Any/Properties.agda b/src/Data/List/Relation/Unary/Any/Properties.agda
index 6383f15a7e..aaba5838e8 100644
--- a/src/Data/List/Relation/Unary/Any/Properties.agda
+++ b/src/Data/List/Relation/Unary/Any/Properties.agda
@@ -25,7 +25,7 @@ open import Data.Nat.Properties using (_≟_; ≤∧≢⇒<; ≤-refl; m<n⇒m<1
 open import Data.Maybe.Base using (Maybe; just; nothing)
 open import Data.Maybe.Relation.Unary.Any as MAny using (just)
 open import Data.Product.Base as Product
-  using (_×_; _,_; ∃; ∃₂; proj₁; proj₂; uncurry′)
+  using (_×_; _,_; ∃; ∃₂; proj₁; proj₂)
 open import Data.Product.Properties
 open import Data.Product.Function.NonDependent.Propositional
   using (_×-cong_)
@@ -41,12 +41,12 @@ open import Level using (Level)
 open import Relation.Binary.Core using (Rel; REL)
 open import Relation.Binary.Definitions as B
 open import Relation.Binary.PropositionalEquality.Core
-  using (_≡_; refl; sym; trans; cong; cong₂; subst)
+  using (_≡_; refl; sym; trans; cong; cong₂; resp)
 open import Relation.Binary.PropositionalEquality.Properties
   using (module ≡-Reasoning)
 open import Relation.Unary as U
   using (Pred; _⟨×⟩_; _⟨→⟩_) renaming (_⊆_ to _⋐_)
-open import Relation.Nullary using (¬_; _because_; does; ofʸ; ofⁿ; yes; no)
+open import Relation.Nullary using (¬_; _because_; does; invert; yes; no)
 open import Relation.Nullary.Decidable using (¬?; decidable-stable)
 open import Relation.Nullary.Negation using (contradiction)
 
@@ -97,6 +97,11 @@ Any-cong {P = P} {Q = Q} {xs = xs} {ys} P↔Q xs≈ys =
 ------------------------------------------------------------------------
 -- Any.map
 
+map-ext : (f g : P ⋐ P) → (∀ {x} (p : P x) → f p ≡ g p) →
+          (p : Any P xs) → Any.map f p ≡ Any.map g p
+map-ext f g hyp (here  p) = cong here (hyp p)
+map-ext f g hyp (there p) = cong there $ map-ext f g hyp p
+
 map-id : ∀ (f : P ⋐ P) → (∀ {x} (p : P x) → f p ≡ p) →
          (p : Any P xs) → Any.map f p ≡ p
 map-id f hyp (here  p) = cong here (hyp p)
@@ -123,29 +128,31 @@ lookup-index (there pxs) = lookup-index pxs
 
 -- Nested occurrences of Any can sometimes be swapped. See also ×↔.
 
-swap : ∀ {P : A → B → Set ℓ} →
-       Any (λ x → Any (P x) ys) xs → Any (λ y → Any (flip P y) xs) ys
-swap (here  pys)  = Any.map here pys
-swap (there pxys) = Any.map there (swap pxys)
+module _ {R : REL A B ℓ} where
+
+  swap : Any (λ x → Any (R x) ys) xs → Any (λ y → Any (flip R y) xs) ys
+  swap (here  pys)  = Any.map here pys
+  swap (there pxys) = Any.map there (swap pxys)
+
+  swap-there : (any : Any (λ x → Any (R x) ys) xs) →
+               swap (Any.map (there {x = x}) any) ≡ there (swap any)
+  swap-there (here  pys)  = refl
+  swap-there (there pxys) = cong (Any.map there) (swap-there pxys)
 
-swap-there : ∀ {P : A → B → Set ℓ} →
-             (any : Any (λ x → Any (P x) ys) xs) →
-             swap (Any.map (there {x = x}) any) ≡ there (swap any)
-swap-there (here  pys)  = refl
-swap-there (there pxys) = cong (Any.map there) (swap-there pxys)
+module _ {R : REL A B ℓ} where
 
-swap-invol : ∀ {P : A → B → Set ℓ} →
-             (any : Any (λ x → Any (P x) ys) xs) →
-             swap (swap any) ≡ any
-swap-invol (here (here px))   = refl
-swap-invol (here (there pys)) =
-  cong (Any.map there) (swap-invol (here pys))
-swap-invol (there pxys)       =
-  trans (swap-there (swap pxys)) (cong there (swap-invol pxys))
+  swap-invol : (any : Any (λ x → Any (R x) ys) xs) →
+               swap (swap any) ≡ any
+  swap-invol (here (here px))   = refl
+  swap-invol (here (there pys)) =
+    cong (Any.map there) (swap-invol (here pys))
+  swap-invol (there pxys)       =
+    trans (swap-there (swap pxys)) (cong there (swap-invol pxys))
 
-swap↔ : ∀ {P : A → B → Set ℓ} →
-       Any (λ x → Any (P x) ys) xs ↔ Any (λ y → Any (flip P y) xs) ys
-swap↔ = mk↔ₛ′ swap swap swap-invol swap-invol
+module _ {R : REL A B ℓ} where
+
+  swap↔ : Any (λ x → Any (R x) ys) xs ↔ Any (λ y → Any (flip R y) xs) ys
+  swap↔ = mk↔ₛ′ swap swap swap-invol swap-invol
 
 ------------------------------------------------------------------------
 -- Lemmas relating Any to ⊥
@@ -213,8 +220,9 @@ Any-×⁺ (p , q) = Any.map (λ p → Any.map (λ q → (p , q)) q) p
 
 Any-×⁻ : Any (λ x → Any (λ y → P x × Q y) ys) xs →
          Any P xs × Any Q ys
-Any-×⁻ pq with Product.map₂ (Product.map₂ find) (find pq)
-... | (x , x∈xs , y , y∈ys , p , q) = lose x∈xs p , lose y∈ys q
+Any-×⁻ pq = let x , x∈xs , pq′ = find pq in
+            let y , y∈ys , p , q = find pq′ in
+            lose x∈xs p , lose y∈ys q
 
 ×↔ : ∀ {xs ys} →
      (Any P xs × Any Q ys) ↔ Any (λ x → Any (λ y → P x × Q y) ys) xs
@@ -255,24 +263,41 @@ Any-×⁻ pq with Product.map₂ (Product.map₂ find) (find pq)
 
     (p , q) ∎
 
-  to∘from : ∀ pq → Any-×⁺ {xs = xs} (Any-×⁻ pq) ≡ pq
-  to∘from pq with find pq
-      | (λ (f : (proj₁ (find pq) ≡_) ⋐ _) → map∘find pq {f})
-  ... | (x , x∈xs , pq′) | lem₁
-    with find pq′
-      | (λ (f : (proj₁ (find pq′) ≡_) ⋐ _) → map∘find pq′ {f})
-  ... | (y , y∈ys , p , q) | lem₂
-    rewrite sym $ map-∘ {R = λ x → Any (λ y → P x × Q y) ys}
-                        (λ p → Any.map (λ q → p , q) (lose y∈ys q))
-                        (λ y → subst P y p)
-                        x∈xs
-            = lem₁ _ helper
-    where
-    helper : Any.map (λ q → p , q) (lose y∈ys q) ≡ pq′
-    helper rewrite sym $ map-∘ (λ q → p , q)
-                               (λ y → subst Q y q)
-                               y∈ys
-           = lem₂ _ refl
+  to∘from : ∀ pq → Any-×⁺ (Any-×⁻ pq) ≡ pq
+  to∘from pq =
+    let x , x∈xs , pq′ = find pq
+
+        lem₁ : {f : (x ≡_) ⋐ λ x → Any (λ y → (P x) × (Q y)) ys} →
+               (f-refl : f refl ≡ pq′) → Any.map f _ ≡ pq
+        lem₁ {f} = map∘find pq {f = f}
+
+        y , y∈ys , p , q = find pq′
+
+        lem₂ : {g : (y ≡_) ⋐ λ y → (P x) × (Q y)} →
+               (g-refl : g refl ≡ (p , q)) → Any.map g _ ≡ pq′
+        lem₂ {g} = map∘find pq′ {f = g}
+
+        helper : Any.map (p ,_) (lose y∈ys q) ≡ pq′
+        helper = begin
+          Any.map (p ,_) (lose y∈ys q)
+            ≡⟨ map-∘ (p ,_) (λ y → resp Q y q) y∈ys ⟨
+          _
+            ≡⟨ lem₂ refl ⟩
+          pq′
+            ∎
+
+        h : P ⋐ λ x → Any (λ y → (P x) × (Q y)) ys
+        h p = Any.map (p ,_) (lose y∈ys q)
+
+    in  begin
+      Any-×⁺ (Any-×⁻ pq)
+        ≡⟨⟩
+      Any.map h (lose x∈xs p)
+        ≡⟨ map-∘ h (λ z → resp P z p) x∈xs ⟨
+      _
+        ≡⟨ lem₁ helper ⟩
+      pq
+        ∎
 
 ------------------------------------------------------------------------
 -- Half-applied product commutes with Any.
@@ -361,9 +386,9 @@ module _ {P : A → Set p} where
   ++⁺∘++⁻ : ∀ xs {ys} (p : Any P (xs ++ ys)) → [ ++⁺ˡ , ++⁺ʳ xs ]′ (++⁻ xs p) ≡ p
   ++⁺∘++⁻ []       p         = refl
   ++⁺∘++⁻ (x ∷ xs) (here  p) = refl
-  ++⁺∘++⁻ (x ∷ xs) (there p) with ++⁻ xs p | ++⁺∘++⁻ xs p
-  ... | inj₁ p′ | ih = cong there ih
-  ... | inj₂ p′ | ih = cong there ih
+  ++⁺∘++⁻ (x ∷ xs) (there p) with ih ← ++⁺∘++⁻ xs p | ++⁻ xs p
+  ... | inj₁ _ = cong there ih
+  ... | inj₂ _ = cong there ih
 
   ++⁻∘++⁺ : ∀ xs {ys} (p : Any P xs ⊎ Any P ys) →
             ++⁻ xs ([ ++⁺ˡ , ++⁺ʳ xs ]′ p) ≡ p
@@ -487,8 +512,8 @@ applyUpTo⁺ f p (s<s i<n@(s≤s _)) =
 applyUpTo⁻ : ∀ f {n} → Any P (applyUpTo f n) →
              ∃ λ i → i < n × P (f i)
 applyUpTo⁻ f {suc n} (here p)  = zero , z<s , p
-applyUpTo⁻ f {suc n} (there p) with applyUpTo⁻ (f ∘ suc) p
-... | i , i<n , q = suc i , s<s i<n , q
+applyUpTo⁻ f {suc n} (there p)
+  with i , i<n , q ← applyUpTo⁻ (f ∘ suc) p = suc i , s<s i<n , q
 
 ------------------------------------------------------------------------
 -- applyDownFrom
@@ -496,13 +521,13 @@ applyUpTo⁻ f {suc n} (there p) with applyUpTo⁻ (f ∘ suc) p
 applyDownFrom⁺ : ∀ f {i n} → P (f i) → i < n → Any P (applyDownFrom f n)
 applyDownFrom⁺ f {i} {suc n} p (s≤s i≤n) with i ≟ n
 ... | yes refl = here p
-... | no  i≢n    = there (applyDownFrom⁺ f p (≤∧≢⇒< i≤n i≢n))
+... | no  i≢n  = there (applyDownFrom⁺ f p (≤∧≢⇒< i≤n i≢n))
 
 applyDownFrom⁻ : ∀ f {n} → Any P (applyDownFrom f n) →
                  ∃ λ i → i < n × P (f i)
 applyDownFrom⁻ f {suc n} (here p)  = n , ≤-refl , p
-applyDownFrom⁻ f {suc n} (there p) with applyDownFrom⁻ f p
-... | i , i<n , pf = i , m<n⇒m<1+n i<n , pf
+applyDownFrom⁻ f {suc n} (there p)
+  with i , i<n , q ← applyDownFrom⁻ f p = i , m<n⇒m<1+n i<n , q
 
 ------------------------------------------------------------------------
 -- tabulate
@@ -522,8 +547,8 @@ module _ (Q? : U.Decidable Q) where
 
   filter⁺ : (p : Any P xs) → Any P (filter Q? xs) ⊎ ¬ Q (Any.lookup p)
   filter⁺ {xs = x ∷ _} (here px) with Q? x
-  ... | true  because _       = inj₁ (here px)
-  ... | false because ofⁿ ¬Qx = inj₂ ¬Qx
+  ... | true  because _     = inj₁ (here px)
+  ... | false because [¬Qx] = inj₂ (invert [¬Qx])
   filter⁺ {xs = x ∷ _} (there p) with does (Q? x)
   ... | true  = Sum.map₁ there (filter⁺ p)
   ... | false = filter⁺ p
@@ -537,14 +562,14 @@ module _ (Q? : U.Decidable Q) where
 ------------------------------------------------------------------------
 -- derun and deduplicate
 
-module _ {R : A → A → Set r} (R? : B.Decidable R) where
+module _ {R : Rel A r} (R? : B.Decidable R) where
 
   private
     derun⁺-aux : ∀ x xs → P Respects R → P x → Any P (derun R? (x ∷ xs))
     derun⁺-aux x [] resp Px = here Px
     derun⁺-aux x (y ∷ xs) resp Px with R? x y
-    ... | true  because ofʸ Rxy = derun⁺-aux y xs resp (resp Rxy Px)
-    ... | false because _       = here Px
+    ... | true  because [Rxy] = derun⁺-aux y xs resp (resp (invert [Rxy]) Px)
+    ... | false because _     = here Px
 
   derun⁺ : P Respects R → Any P xs → Any P (derun R? xs)
   derun⁺ {xs = x ∷ xs}     resp (here px)   = derun⁺-aux x xs resp px

From 4e8fb9345102e2a05a0b50bfa0e9e6cf4d30b537 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 21 Mar 2024 09:15:01 +0000
Subject: [PATCH 11/47] knock-on viscosity

---
 .../List/Relation/Unary/All/Properties.agda   | 40 +++++++++----------
 1 file changed, 20 insertions(+), 20 deletions(-)

diff --git a/src/Data/List/Relation/Unary/All/Properties.agda b/src/Data/List/Relation/Unary/All/Properties.agda
index a36a07f3b1..fee1579193 100644
--- a/src/Data/List/Relation/Unary/All/Properties.agda
+++ b/src/Data/List/Relation/Unary/All/Properties.agda
@@ -14,19 +14,19 @@ open import Data.Bool.Properties using (T-∧)
 open import Data.Empty
 open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.List.Base as List hiding (lookup; updateAt)
-open import Data.List.Properties as Listₚ using (partition-defn)
 open import Data.List.Membership.Propositional
 open import Data.List.Membership.Propositional.Properties
 import Data.List.Membership.Setoid as SetoidMembership
+import Data.List.Properties as List
+import Data.List.Relation.Binary.Equality.Setoid as ≋
+open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; []; _∷_)
+open import Data.List.Relation.Binary.Subset.Propositional using (_⊆_)
 open import Data.List.Relation.Unary.All as All using
   ( All; []; _∷_; lookup; updateAt
   ; _[_]=_; here; there
   ; Null
   )
 open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
-import Data.List.Relation.Binary.Equality.Setoid as ListEq using (_≋_; []; _∷_)
-open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; []; _∷_)
-open import Data.List.Relation.Binary.Subset.Propositional using (_⊆_)
 open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
 open import Data.Maybe.Relation.Unary.All as Maybe using (just; nothing; fromAny)
 open import Data.Maybe.Relation.Unary.Any as Maybe using (just)
@@ -523,7 +523,7 @@ takeWhile⁺ {xs = x ∷ xs} Q? (px ∷ pxs) with does (Q? x)
 takeWhile⁻ : (P? : Decidable P) → takeWhile P? xs ≡ xs → All P xs
 takeWhile⁻ {xs = []}     P? eq = []
 takeWhile⁻ {xs = x ∷ xs} P? eq with P? x
-... | yes px = px ∷ takeWhile⁻ P? (Listₚ.∷-injectiveʳ eq)
+... | yes px = px ∷ takeWhile⁻ P? (List.∷-injectiveʳ eq)
 ... | no ¬px = case eq of λ ()
 
 all-takeWhile : (P? : Decidable P) → ∀ xs → All P (takeWhile P? xs)
@@ -595,7 +595,7 @@ module _ (P? : Decidable P) where
   all-filter : ∀ xs → All P (filter P? xs)
   all-filter []       = []
   all-filter (x ∷ xs) with P? x
-  ... |  true because [Px] = invert [Px] ∷ all-filter xs
+  ... | true  because [Px] = invert [Px] ∷ all-filter xs
   ... | false because  _   = all-filter xs
 
   filter⁺ : All Q xs → All Q (filter P? xs)
@@ -605,12 +605,12 @@ module _ (P? : Decidable P) where
   ... | true  = Qx ∷ filter⁺ Qxs
 
   filter⁻ : All Q (filter P? xs) → All Q (filter (¬? ∘ P?) xs) → All Q xs
-  filter⁻ {xs = []}           []          []                           = []
-  filter⁻ {xs = x ∷ xs}       all⁺        all⁻ with P? x  | ¬? (P? x)
-  filter⁻ {xs = x ∷ xs}       all⁺        all⁻  | yes  Px | yes  ¬Px = contradiction Px ¬Px
-  filter⁻ {xs = x ∷ xs} (qx ∷ all⁺)       all⁻  | yes  Px | no  ¬¬Px = qx ∷ filter⁻ all⁺ all⁻
-  filter⁻ {xs = x ∷ xs}       all⁺  (qx ∷ all⁻) | no    _ | yes  ¬Px = qx ∷ filter⁻ all⁺ all⁻
-  filter⁻ {xs = x ∷ xs}       all⁺        all⁻  | no  ¬Px | no  ¬¬Px = contradiction ¬Px ¬¬Px
+  filter⁻ {xs = []}          []          []                         = []
+  filter⁻ {xs = x ∷ _}       all⁺        all⁻ with P? x  | ¬? (P? x)
+  filter⁻ {xs = x ∷ _}       all⁺        all⁻  | yes  Px | yes  ¬Px = contradiction Px ¬Px
+  filter⁻ {xs = x ∷ _} (qx ∷ all⁺)       all⁻  | yes  Px | no  ¬¬Px = qx ∷ filter⁻ all⁺ all⁻
+  filter⁻ {xs = x ∷ _}       all⁺  (qx ∷ all⁻) | no    _ | yes  ¬Px = qx ∷ filter⁻ all⁺ all⁻
+  filter⁻ {xs = x ∷ _}       all⁺        all⁻  | no  ¬Px | no  ¬¬Px = contradiction ¬Px ¬¬Px
 
 ------------------------------------------------------------------------
 -- partition
@@ -619,7 +619,7 @@ module _ {P : A → Set p} (P? : Decidable P) where
 
   partition-All : ∀ xs → (let ys , zs = partition P? xs) →
                   All P ys × All (∁ P) zs
-  partition-All xs rewrite partition-defn P? xs =
+  partition-All xs rewrite List.partition-defn P? xs =
     all-filter P? xs , all-filter (∁? P?) xs
 
 ------------------------------------------------------------------------
@@ -635,7 +635,7 @@ module _ {R : A → A → Set q} (R? : B.Decidable R) where
   ... | true  = derun⁺ all[P,y∷xs]
 
   deduplicate⁺ : All P xs → All P (deduplicate R? xs)
-  deduplicate⁺ []               = []
+  deduplicate⁺ []         = []
   deduplicate⁺ (px ∷ pxs) = px ∷ filter⁺ (¬? ∘ R? _) (deduplicate⁺ pxs)
 
   derun⁻ : P B.Respects (flip R) → ∀ xs → All P (derun R? xs) → All P xs
@@ -645,8 +645,8 @@ module _ {R : A → A → Set q} (R? : B.Decidable R) where
     aux : ∀ x xs → All P (derun R? (x ∷ xs)) → All P (x ∷ xs)
     aux x []       (px ∷ []) = px ∷ []
     aux x (y ∷ xs) all[P,x∷y∷xs] with R? x y
-    aux x (y ∷ xs) all[P,y∷xs]        | yes Rxy with aux y xs all[P,y∷xs]
-    aux x (y ∷ xs) all[P,y∷xs]        | yes Rxy | r@(py ∷ _) = P-resp-R Rxy py ∷ r
+    aux x (y ∷ xs) all[P,y∷xs]        | yes Rxy
+      with r@(py ∷ _) ← aux y xs all[P,y∷xs] = P-resp-R Rxy py ∷ r
     aux x (y ∷ xs) (px ∷ all[P,y∷xs]) | no _ = px ∷ aux y xs all[P,y∷xs]
 
   deduplicate⁻ : P B.Respects R → ∀ xs → All P (deduplicate R? xs) → All P xs
@@ -719,9 +719,9 @@ tails⁻ (x ∷ xs) (pxxs ∷ _) = pxxs
 module _ (p : A → Bool) where
 
   all⁺ : ∀ xs → T (all p xs) → All (T ∘ p) xs
-  all⁺ []       _     = []
-  all⁺ (x ∷ xs) px∷xs with Equivalence.to (T-∧ {p x}) px∷xs
-  ... | (px , pxs) = px ∷ all⁺ xs pxs
+  all⁺ []       _      = []
+  all⁺ (x ∷ xs) px∷pxs
+    with px , pxs ← Equivalence.to (T-∧ {p x}) px∷pxs = px ∷ all⁺ xs pxs
 
   all⁻ : All (T ∘ p) xs → T (all p xs)
   all⁻ []         = _
@@ -743,7 +743,7 @@ all-anti-mono p xs⊆ys = all⁻ p ∘ anti-mono xs⊆ys ∘ all⁺ p _
 module _ (S : Setoid c ℓ) where
 
   open Setoid S
-  open ListEq S
+  open ≋ S
 
   respects : P B.Respects _≈_ → (All P) B.Respects _≋_
   respects p≈ []            []         = []

From aebe82862cc505152f64cdb4a5434880f6722b14 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 21 Mar 2024 09:26:54 +0000
Subject: [PATCH 12/47] tightened `import`s

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

diff --git a/src/Data/List/Relation/Unary/All.agda b/src/Data/List/Relation/Unary/All.agda
index 3c6cfa0b49..16a7be9d69 100644
--- a/src/Data/List/Relation/Unary/All.agda
+++ b/src/Data/List/Relation/Unary/All.agda
@@ -8,9 +8,6 @@
 
 module Data.List.Relation.Unary.All where
 
-open import Effect.Applicative
-open import Effect.Monad
-open import Data.Empty using (⊥)
 open import Data.List.Base as List using (List; []; _∷_)
 open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
 open import Data.List.Membership.Propositional renaming (_∈_ to _∈ₚ_; ∀∈ to ∀∈ₚ)
@@ -18,6 +15,8 @@ import Data.List.Membership.Setoid as SetoidMembership
 open import Data.Product.Base as Product
   using (∃; -,_; _×_; _,_; proj₁; proj₂; uncurry)
 open import Data.Sum.Base as Sum using (inj₁; inj₂)
+open import Effect.Applicative
+open import Effect.Monad
 open import Function.Base using (_∘_; _∘′_; id; const)
 open import Level using (Level; _⊔_)
 open import Relation.Nullary hiding (Irrelevant)

From 7a744ec8768ca9b2b96c98fa3d58924eb166e7b9 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 21 Mar 2024 09:44:49 +0000
Subject: [PATCH 13/47] misc. import and other tweaks

---
 .../List/Membership/Setoid/Properties.agda    | 53 +++++++++----------
 1 file changed, 26 insertions(+), 27 deletions(-)

diff --git a/src/Data/List/Membership/Setoid/Properties.agda b/src/Data/List/Membership/Setoid/Properties.agda
index c06897367b..3e6942f5cb 100644
--- a/src/Data/List/Membership/Setoid/Properties.agda
+++ b/src/Data/List/Membership/Setoid/Properties.agda
@@ -13,15 +13,14 @@ open import Data.Bool.Base using (true; false)
 open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.Fin.Properties using (suc-injective)
 open import Data.List.Base hiding (find)
-open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
-open import Data.List.Relation.Unary.All as All using (All)
-import Data.List.Relation.Unary.Any.Properties as Any
 import Data.List.Membership.Setoid as Membership
 import Data.List.Relation.Binary.Equality.Setoid as Equality
+open import Data.List.Relation.Unary.All as All using (All)
+open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
+import Data.List.Relation.Unary.Any.Properties as Any
 import Data.List.Relation.Unary.Unique.Setoid as Unique
-open import Data.Nat.Base using (suc; z≤n; s≤s; _≤_; _<_)
-open import Data.Nat.Properties using (≤-trans; n≤1+n)
-open import Data.Product.Base as Product using (∃; _×_; _,_ ; ∃₂; proj₁; proj₂)
+open import Data.Nat.Base using (suc; z<s; _<_)
+open import Data.Product.Base as Product using (∃; _×_; _,_ ; ∃₂)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Function.Base using (_$_; flip; _∘_; _∘′_; id)
@@ -31,11 +30,11 @@ open import Relation.Binary.Core using (Rel; _Preserves₂_⟶_⟶_; _Preserves_
 open import Relation.Binary.Definitions as Binary hiding (Decidable)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
-open import Relation.Unary as Unary using (Decidable; Pred)
-open import Relation.Nullary using (¬_; does; _because_; yes; no)
+open import Relation.Nullary.Decidable using (does; _because_; yes; no)
+open import Relation.Nullary.Negation using (¬_; contradiction)
 open import Relation.Nullary.Reflects using (invert)
-open import Relation.Nullary.Negation using (contradiction)
-open import Relation.Nullary.Decidable using (¬?)
+open import Relation.Unary as Unary using (Decidable; Pred)
+
 open Setoid using (Carrier)
 
 private
@@ -148,24 +147,24 @@ module _ (S : Setoid c ℓ) where
 
 module _ (S₁ : Setoid c₁ ℓ₁) (S₂ : Setoid c₂ ℓ₂) where
 
-  open Setoid S₁ renaming (Carrier to A₁; _≈_ to _≈₁_; refl to refl₁)
-  open Setoid S₂ renaming (Carrier to A₂; _≈_ to _≈₂_)
+  open Setoid S₁ renaming (_≈_ to _≈₁_)
+  open Setoid S₂ renaming (_≈_ to _≈₂_)
   private module M₁ = Membership S₁; open M₁ using (find) renaming (_∈_ to _∈₁_)
   private module M₂ = Membership S₂; open M₂ using () renaming (_∈_ to _∈₂_)
 
-  ∈-map⁺ : ∀ {f} → f Preserves _≈₁_ ⟶ _≈₂_ → ∀ {v xs} →
-            v ∈₁ xs → f v ∈₂ map f xs
+  ∈-map⁺ : ∀ {f} → f Preserves _≈₁_ ⟶ _≈₂_ →
+           ∀ {v xs} → v ∈₁ xs → f v ∈₂ map f xs
   ∈-map⁺ pres x∈xs = Any.map⁺ (Any.map pres x∈xs)
 
   ∈-map⁻ : ∀ {v xs f} → v ∈₂ map f xs →
            ∃ λ x → x ∈₁ xs × v ≈₂ f x
   ∈-map⁻ x∈map = find (Any.map⁻ x∈map)
 
-  map-∷= : ∀ {f} (f≈ : f Preserves _≈₁_ ⟶ _≈₂_)
-           {xs x v} → (x∈xs : x ∈₁ xs) →
-           map f (x∈xs M₁.∷= v) ≡ ∈-map⁺ f≈ x∈xs M₂.∷= f v
-  map-∷= f≈ (here x≈y)   = ≡.refl
-  map-∷= f≈ (there x∈xs) = ≡.cong (_ ∷_) (map-∷= f≈ x∈xs)
+  map-∷= : ∀ {f} (pres : f Preserves _≈₁_ ⟶ _≈₂_) →
+           ∀ {xs x v} → (x∈xs : x ∈₁ xs) →
+           map f (x∈xs M₁.∷= v) ≡ ∈-map⁺ pres x∈xs M₂.∷= f v
+  map-∷= pres (here x≈y)   = ≡.refl
+  map-∷= pres (there x∈xs) = ≡.cong (_ ∷_) (map-∷= pres x∈xs)
 
 ------------------------------------------------------------------------
 -- _++_
@@ -211,9 +210,9 @@ module _ (S : Setoid c ℓ) where
 
   ∈-∃++ : ∀ {v xs} → v ∈ xs → ∃₂ λ ys zs → ∃ λ w →
           v ≈ w × xs ≋ ys ++ [ w ] ++ zs
-  ∈-∃++ (here px)                  = [] , _ , _ , px , ≋-refl
-  ∈-∃++ (there {d} v∈xs) with ∈-∃++ v∈xs
-  ... | hs , _ , _ , v≈v′ , eq = d ∷ hs , _ , _ , v≈v′ , refl ∷ eq
+  ∈-∃++ (here px)        = [] , _ , _ , px , ≋-refl
+  ∈-∃++ (there {d} v∈xs) with hs , _ , _ , v≈v′ , eq ← ∈-∃++ v∈xs
+                         = d ∷ hs , _ , _ , v≈v′ , refl ∷ eq
 
 ------------------------------------------------------------------------
 -- concat
@@ -235,8 +234,8 @@ module _ (S : Setoid c ℓ) where
   ∈-concat⁺′ v∈vs = ∈-concat⁺ ∘ Any.map (flip (∈-resp-≋ S) v∈vs)
 
   ∈-concat⁻′ : ∀ {v} xss → v ∈ concat xss → ∃ λ xs → v ∈ xs × xs ∈ₗ xss
-  ∈-concat⁻′ xss v∈c[xss] with find (∈-concat⁻ xss v∈c[xss])
-  ... | xs , t , s = xs , s , t
+  ∈-concat⁻′ xss v∈c[xss]
+    with xs , xs∈xss , v∈xs ← find (∈-concat⁻ xss v∈c[xss]) = xs , v∈xs , xs∈xss
 
 ------------------------------------------------------------------------
 -- cartesianProductWith
@@ -375,9 +374,9 @@ module _ (S : Setoid c ℓ) where
 
   open Membership S using (_∈_)
 
-  ∈-length : ∀ {x xs} → x ∈ xs → 1 ≤ length xs
-  ∈-length (here px)    = s≤s z≤n
-  ∈-length (there x∈xs) = ≤-trans (∈-length x∈xs) (n≤1+n _)
+  ∈-length : ∀ {x xs} → x ∈ xs → 0 < length xs
+  ∈-length (here px)    = z<s
+  ∈-length (there x∈xs) = z<s
 
 ------------------------------------------------------------------------
 -- lookup

From 5b921bdd6b2ffec09da5c63c103c45f443583673 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 21 Mar 2024 09:47:09 +0000
Subject: [PATCH 14/47] misc. import and other tweaks

---
 src/Data/List/Membership/Setoid.agda | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/Data/List/Membership/Setoid.agda b/src/Data/List/Membership/Setoid.agda
index 9919bf9409..ce8ab13570 100644
--- a/src/Data/List/Membership/Setoid.agda
+++ b/src/Data/List/Membership/Setoid.agda
@@ -7,17 +7,17 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Relation.Binary.Bundles using (Setoid)
-open import Relation.Binary.Definitions using (_Respects_)
 
 module Data.List.Membership.Setoid {c ℓ} (S : Setoid c ℓ) where
 
-open import Function.Base using (_∘_; id; flip; const)
-open import Data.List.Base as List using (List; []; _∷_; length; lookup)
+open import Data.List.Base using (List; []; _∷_; length; lookup)
 open import Data.List.Relation.Unary.Any as Any
   using (Any; index; map; here; there)
 open import Data.Product.Base as Product using (∃; _×_; _,_)
-open import Relation.Unary using (Pred)
+open import Function.Base using (_∘_; id; flip; const)
+open import Relation.Binary.Definitions using (_Respects_)
 open import Relation.Nullary.Negation using (¬_)
+open import Relation.Unary using (Pred)
 
 open Setoid S renaming (Carrier to A)
 
@@ -57,7 +57,7 @@ module _ {p} {P : Pred A p} where
   find : ∀ {xs} → Any P xs → ∃∈ P xs
   find (here px)   = _ , here refl , px
   find (there pxs) = Product.map id (Product.map there id) (find pxs)
-  -- let x , x∈xs , px = find pxs in x , there x∈xs , px
+  -- better? let x , x∈xs , px = find pxs in x , there x∈xs , px
 
   lose : P Respects _≈_ →  ∀ {x xs} → x ∈ xs → P x → Any P xs
   lose resp x∈xs px = map (flip resp px) x∈xs

From 914c980856ae9b946b1b8285b05545b2863680bc Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 21 Mar 2024 09:55:47 +0000
Subject: [PATCH 15/47] misc. import and other tweaks

---
 .../Membership/Propositional/Properties.agda  | 77 +++++++++----------
 .../Propositional/Properties/Core.agda        |  2 +-
 2 files changed, 39 insertions(+), 40 deletions(-)

diff --git a/src/Data/List/Membership/Propositional/Properties.agda b/src/Data/List/Membership/Propositional/Properties.agda
index c5ab013b61..5fef487583 100644
--- a/src/Data/List/Membership/Propositional/Properties.agda
+++ b/src/Data/List/Membership/Propositional/Properties.agda
@@ -9,24 +9,25 @@
 module Data.List.Membership.Propositional.Properties where
 
 open import Algebra using (Op₂; Selective)
-open import Effect.Monad using (RawMonad)
-open import Data.Bool.Base using (Bool; false; true; T)
+open import Data.Bool.Base using (Bool; false; true; if_then_else_)
 open import Data.Fin.Base using (Fin)
 open import Data.List.Base as List
-open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
-open import Data.List.Relation.Unary.Any.Properties
+open import Data.List.Effectful using (monad)
 open import Data.List.Membership.Propositional
 import Data.List.Membership.Setoid.Properties as Membership
 open import Data.List.Relation.Binary.Equality.Propositional
   using (_≋_; ≡⇒≋; ≋⇒≡)
-open import Data.List.Effectful using (monad)
-open import Data.Nat.Base using (ℕ; zero; suc; pred; s≤s; _≤_; _<_; _≤ᵇ_)
+open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
+open import Data.List.Relation.Unary.Any.Properties
+open import Data.Nat.Base using (ℕ; suc; s≤s; _≤_; _<_; _≰_)
 open import Data.Nat.Properties
+  using (suc-injective; m≤n⇒m≤1+n; _≤?_; <⇒≢; ≰⇒>)
 open import Data.Product.Base hiding (map)
 open import Data.Product.Properties using (×-≡,≡↔≡)
 open import Data.Product.Function.NonDependent.Propositional using (_×-cong_)
 import Data.Product.Function.Dependent.Propositional as Σ
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
+open import Effect.Monad using (RawMonad)
 open import Function.Base
 open import Function.Definitions
 import Function.Related.Propositional as Related
@@ -37,14 +38,12 @@ open import Level using (Level)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Definitions as Binary hiding (Decidable)
 open import Relation.Binary.PropositionalEquality as ≡
-  using (_≡_; _≢_; refl; sym; trans; cong; subst; →-to-⟶; _≗_)
+  using (_≡_; _≢_; refl; sym; trans; cong; resp; →-to-⟶; _≗_)
 import Relation.Binary.Properties.DecTotalOrder as DTOProperties
-open import Relation.Unary using (_⟨×⟩_; Decidable)
-import Relation.Nullary.Reflects as Reflects
+open import Relation.Nullary.Decidable using (Dec; does; yes; no; ¬¬-excluded-middle)
+open import Relation.Nullary.Negation using (¬_; contradiction)
 open import Relation.Nullary.Reflects using (invert)
-open import Relation.Nullary using (¬_; Dec; does; yes; no; _because_)
-open import Relation.Nullary.Negation using (contradiction)
-open import Relation.Nullary.Decidable using (¬¬-excluded-middle)
+open import Relation.Unary using (_⟨×⟩_; Decidable)
 
 private
   open module ListMonad {ℓ} = RawMonad (monad {ℓ = ℓ})
@@ -56,7 +55,7 @@ private
 ------------------------------------------------------------------------
 -- Publicly re-export properties from Core
 
-open import Data.List.Membership.Propositional.Properties.Core public
+open import Data.List.Membership.Propositional.Properties.CoreNEW public
 
 ------------------------------------------------------------------------
 -- Equality
@@ -124,8 +123,9 @@ module _ {v : A} where
   ∈-insert xs = Membership.∈-insert (≡.setoid A) xs refl
 
   ∈-∃++ : ∀ {xs} → v ∈ xs → ∃₂ λ ys zs → xs ≡ ys ++ [ v ] ++ zs
-  ∈-∃++ v∈xs with Membership.∈-∃++ (≡.setoid A) v∈xs
-  ... | ys , zs , _ , refl , eq = ys , zs , ≋⇒≡ eq
+  ∈-∃++ v∈xs
+    with ys , zs , _ , refl , eq ← Membership.∈-∃++ (≡.setoid A) v∈xs
+    = ys , zs , ≋⇒≡ eq
 
 ------------------------------------------------------------------------
 -- concat
@@ -143,8 +143,9 @@ module _ {v : A} where
     Membership.∈-concat⁺′ (≡.setoid A) v∈vs (Any.map ≡⇒≋ vs∈xss)
 
   ∈-concat⁻′ : ∀ xss → v ∈ concat xss → ∃ λ xs → v ∈ xs × xs ∈ xss
-  ∈-concat⁻′ xss v∈c with Membership.∈-concat⁻′ (≡.setoid A) xss v∈c
-  ... | xs , v∈xs , xs∈xss = xs , v∈xs , Any.map ≋⇒≡ xs∈xss
+  ∈-concat⁻′ xss v∈c
+    with xs , v∈xs , xs∈xss ← Membership.∈-concat⁻′ (≡.setoid A) xss v∈c
+    = xs , v∈xs , Any.map ≋⇒≡ xs∈xss
 
   concat-∈↔ : ∀ {xss : List (List A)} →
               (∃ λ xs → v ∈ xs × xs ∈ xss) ↔ v ∈ concat xss
@@ -179,8 +180,9 @@ module _ (f : A → B → C) where
 
 ∈-cartesianProduct⁻ : ∀ xs ys {xy@(x , y) : A × B} →
                       xy ∈ cartesianProduct xs ys → x ∈ xs × y ∈ ys
-∈-cartesianProduct⁻ xs ys xy∈p[xs,ys] with ∈-cartesianProductWith⁻ _,_ xs ys xy∈p[xs,ys]
-... | (x , y , x∈xs , y∈ys , refl) = x∈xs , y∈ys
+∈-cartesianProduct⁻ xs ys xy∈p[xs,ys]
+  with _ , _ , x∈xs , y∈ys , refl ← ∈-cartesianProductWith⁻ _,_ xs ys xy∈p[xs,ys]
+  = x∈xs , y∈ys
 
 ------------------------------------------------------------------------
 -- applyUpTo
@@ -201,8 +203,7 @@ module _ (f : ℕ → A) where
 ∈-upTo⁺ = ∈-applyUpTo⁺ id
 
 ∈-upTo⁻ : ∀ {n i} → i ∈ upTo n → i < n
-∈-upTo⁻ p with ∈-applyUpTo⁻ id p
-... | _ , i<n , refl = i<n
+∈-upTo⁻ p with _ , i<n , refl ← ∈-applyUpTo⁻ id p = i<n
 
 ------------------------------------------------------------------------
 -- applyDownFrom
@@ -223,8 +224,7 @@ module _ (f : ℕ → A) where
 ∈-downFrom⁺ i<n = ∈-applyDownFrom⁺ id i<n
 
 ∈-downFrom⁻ : ∀ {n i} → i ∈ downFrom n → i < n
-∈-downFrom⁻ p with ∈-applyDownFrom⁻ id p
-... | _ , i<n , refl = i<n
+∈-downFrom⁻ p with _ , i<n , refl ← ∈-applyDownFrom⁻ id p = i<n
 
 ------------------------------------------------------------------------
 -- tabulate
@@ -243,10 +243,10 @@ module _ {n} {f : Fin n → A} where
 module _ {p} {P : A → Set p} (P? : Decidable P) where
 
   ∈-filter⁺ : ∀ {x xs} → x ∈ xs → P x → x ∈ filter P? xs
-  ∈-filter⁺ = Membership.∈-filter⁺ (≡.setoid A) P? (≡.subst P)
+  ∈-filter⁺ = Membership.∈-filter⁺ (≡.setoid A) P? (≡.resp P)
 
   ∈-filter⁻ : ∀ {v xs} → v ∈ filter P? xs → v ∈ xs × P v
-  ∈-filter⁻ = Membership.∈-filter⁻ (≡.setoid A) P? (≡.subst P)
+  ∈-filter⁻ = Membership.∈-filter⁻ (≡.setoid A) P? (≡.resp P)
 
 ------------------------------------------------------------------------
 -- derun and deduplicate
@@ -306,7 +306,7 @@ module _ (_≈?_ : Binary.Decidable {A = A} _≡_) where
 ------------------------------------------------------------------------
 -- length
 
-∈-length : ∀ {x : A} {xs} → x ∈ xs → 1 ≤ length xs
+∈-length : ∀ {x : A} {xs} → x ∈ xs → 0 < length xs
 ∈-length = Membership.∈-length (≡.setoid _)
 
 ------------------------------------------------------------------------
@@ -362,28 +362,27 @@ finite inj (x ∷ xs) fᵢ∈x∷xs = ¬¬-excluded-middle helper
   helper (yes (i , fᵢ≡x)) = finite f′-inj xs f′ⱼ∈xs
     where
     f′ : ℕ → _
-    f′ j with does (i ≤? j)
-    ... | true  = f (suc j)
-    ... | false = f j
+    f′ j with i ≤? j
+    ... | yes _ = f (suc j)
+    ... | no  _ = f j
 
     ∈-if-not-i : ∀ {j} → i ≢ j → f j ∈ xs
     ∈-if-not-i i≢j = not-x (i≢j ∘ f-inj ∘ trans fᵢ≡x ∘ sym)
 
-    lemma : ∀ {k j} → i ≤ j → ¬ (i ≤ k) → suc j ≢ k
+    lemma : ∀ {k j} → i ≤ j → i ≰ k → suc j ≢ k
     lemma i≤j i≰1+j refl = i≰1+j (m≤n⇒m≤1+n i≤j)
 
     f′ⱼ∈xs : ∀ j → f′ j ∈ xs
-    f′ⱼ∈xs j with i ≤ᵇ j | Reflects.invert (≤ᵇ-reflects-≤ i j)
-    ... | true  | p = ∈-if-not-i (<⇒≢ (s≤s p))
-    ... | false | p = ∈-if-not-i (<⇒≢ (≰⇒> p) ∘ sym)
+    f′ⱼ∈xs j with i ≤? j
+    ... | yes i≤j = ∈-if-not-i (<⇒≢ (s≤s i≤j))
+    ... | no  i≰j = ∈-if-not-i (<⇒≢ (≰⇒> i≰j) ∘ sym)
 
     f′-injective′ : Injective _≡_ _≡_ f′
-    f′-injective′ {j} {k} eq with i ≤ᵇ j | Reflects.invert (≤ᵇ-reflects-≤ i j)
-                                | i ≤ᵇ k | Reflects.invert (≤ᵇ-reflects-≤ i k)
-    ... | true  | p | true  | q = ≡.cong pred (f-inj eq)
-    ... | true  | p | false | q = contradiction (f-inj eq) (lemma p q)
-    ... | false | p | true  | q = contradiction (f-inj eq) (lemma q p ∘ sym)
-    ... | false | p | false | q = f-inj eq
+    f′-injective′ {j} {k} eq with i ≤? j | i ≤? k
+    ... | yes i≤j | yes i≤k = suc-injective (f-inj eq)
+    ... | yes i≤j | no  i≰k = contradiction (f-inj eq) (lemma i≤j i≰k)
+    ... | no  i≰j | yes i≤k = contradiction (f-inj eq) (lemma i≤k i≰j ∘ sym)
+    ... | no  i≰j | no  i≰k = f-inj eq
 
     f′-inj : ℕ ↣ _
     f′-inj = record
diff --git a/src/Data/List/Membership/Propositional/Properties/Core.agda b/src/Data/List/Membership/Propositional/Properties/Core.agda
index 27a29081cd..9273630b4f 100644
--- a/src/Data/List/Membership/Propositional/Properties/Core.agda
+++ b/src/Data/List/Membership/Propositional/Properties/Core.agda
@@ -13,8 +13,8 @@
 module Data.List.Membership.Propositional.Properties.Core where
 
 open import Data.List.Base using (List)
-open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
 open import Data.List.Membership.Propositional
+open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
 open import Data.Product.Base as Product using (_,_)
 open import Function.Base using (flip; id; _∘_)
 open import Function.Bundles using (_↔_; mk↔ₛ′)

From 82e3da00c0931215ddd741480c6bb7150eef7c1a Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 21 Mar 2024 11:57:01 +0000
Subject: [PATCH 16/47] removed spurious module name

---
 src/Data/List/Membership/Propositional/Properties.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/List/Membership/Propositional/Properties.agda b/src/Data/List/Membership/Propositional/Properties.agda
index 5fef487583..40f4792230 100644
--- a/src/Data/List/Membership/Propositional/Properties.agda
+++ b/src/Data/List/Membership/Propositional/Properties.agda
@@ -55,7 +55,7 @@ private
 ------------------------------------------------------------------------
 -- Publicly re-export properties from Core
 
-open import Data.List.Membership.Propositional.Properties.CoreNEW public
+open import Data.List.Membership.Propositional.Properties.Core public
 
 ------------------------------------------------------------------------
 -- Equality

From 617d4a83745f6632767117c6a56bcb0838dffd01 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Fri, 22 Mar 2024 13:55:53 +0000
Subject: [PATCH 17/47] better definition of `find`

---
 src/Data/List/Membership/Setoid.agda | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/Data/List/Membership/Setoid.agda b/src/Data/List/Membership/Setoid.agda
index ce8ab13570..3cce430778 100644
--- a/src/Data/List/Membership/Setoid.agda
+++ b/src/Data/List/Membership/Setoid.agda
@@ -56,8 +56,7 @@ module _ {p} {P : Pred A p} where
 
   find : ∀ {xs} → Any P xs → ∃∈ P xs
   find (here px)   = _ , here refl , px
-  find (there pxs) = Product.map id (Product.map there id) (find pxs)
-  -- better? let x , x∈xs , px = find pxs in x , there x∈xs , px
+  find (there pxs) = let x , x∈xs , px = find pxs in x , there x∈xs , px
 
   lose : P Respects _≈_ →  ∀ {x xs} → x ∈ xs → P x → Any P xs
   lose resp x∈xs px = map (flip resp px) x∈xs

From b111a970e9acf5d1e0d131a6d59a0ae19d768d5a Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Fri, 22 Mar 2024 14:31:53 +0000
Subject: [PATCH 18/47] =?UTF-8?q?make=20intermediate=20terms=20explicit=20?=
 =?UTF-8?q?in=20proof=20of=20`to=E2=88=98from`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Data/List/Relation/Unary/Any/Properties.agda | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Data/List/Relation/Unary/Any/Properties.agda b/src/Data/List/Relation/Unary/Any/Properties.agda
index aaba5838e8..ee54b30cb1 100644
--- a/src/Data/List/Relation/Unary/Any/Properties.agda
+++ b/src/Data/List/Relation/Unary/Any/Properties.agda
@@ -280,8 +280,8 @@ Any-×⁻ pq = let x , x∈xs , pq′ = find pq in
         helper : Any.map (p ,_) (lose y∈ys q) ≡ pq′
         helper = begin
           Any.map (p ,_) (lose y∈ys q)
-            ≡⟨ map-∘ (p ,_) (λ y → resp Q y q) y∈ys ⟨
-          _
+            ≡⟨ map-∘ (p ,_) (λ z → resp Q z q) y∈ys ⟨
+          Any.map (λ z → p , resp Q z q) y∈ys
             ≡⟨ lem₂ refl ⟩
           pq′
             ∎
@@ -294,7 +294,7 @@ Any-×⁻ pq = let x , x∈xs , pq′ = find pq in
         ≡⟨⟩
       Any.map h (lose x∈xs p)
         ≡⟨ map-∘ h (λ z → resp P z p) x∈xs ⟨
-      _
+      Any.map (λ z → Any.map (resp P z p ,_) (lose y∈ys q)) x∈xs
         ≡⟨ lem₁ helper ⟩
       pq
         ∎

From 1afcb6d9e5b019f022aca78a168e41b764a8f08f Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Fri, 22 Mar 2024 14:45:25 +0000
Subject: [PATCH 19/47] tweaks

---
 src/Data/List/Relation/Unary/Any/Properties.agda | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Data/List/Relation/Unary/Any/Properties.agda b/src/Data/List/Relation/Unary/Any/Properties.agda
index ee54b30cb1..9b85d362e6 100644
--- a/src/Data/List/Relation/Unary/Any/Properties.agda
+++ b/src/Data/List/Relation/Unary/Any/Properties.agda
@@ -231,7 +231,7 @@ Any-×⁻ pq = let x , x∈xs , pq′ = find pq in
   open ≡-Reasoning
 
   from∘to : ∀ pq → Any-×⁻ (Any-×⁺ pq) ≡ pq
-  from∘to (p , q) =
+  from∘to (p , q) = let x , x∈xs , px = find p in
 
     Any-×⁻ (Any-×⁺ (p , q))
 
@@ -250,10 +250,10 @@ Any-×⁻ pq = let x , x∈xs , pq′ = find pq in
          (y , y∈ys , p , q) = find (Any.map (p ,_) q)
      in  lose x∈xs p , lose y∈ys q)
 
-     ≡⟨ cong (λ • → let (x , x∈xs , p)     = find p
+     ≡⟨ cong (λ • → let (x , x∈xs , _)     = find p
                         (y , y∈ys , p , q) = •
                     in  lose x∈xs p , lose y∈ys q)
-             (find∘map q (proj₂ (proj₂ (find p)) ,_)) ⟩
+             (find∘map q (px ,_)) ⟩
 
     (let (x , x∈xs , p) = find p
          (y , y∈ys , q) = find q

From 374008bf9bb7ee3cbfde29bdbb24139849394fbd Mon Sep 17 00:00:00 2001
From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Date: Fri, 22 Mar 2024 15:53:17 +0000
Subject: [PATCH 20/47] Update Setoid.agda

Remove redundant import of `index` from `Any`
---
 src/Data/List/Membership/Setoid.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/List/Membership/Setoid.agda b/src/Data/List/Membership/Setoid.agda
index 3cce430778..a88f242b20 100644
--- a/src/Data/List/Membership/Setoid.agda
+++ b/src/Data/List/Membership/Setoid.agda
@@ -12,7 +12,7 @@ module Data.List.Membership.Setoid {c ℓ} (S : Setoid c ℓ) where
 
 open import Data.List.Base using (List; []; _∷_; length; lookup)
 open import Data.List.Relation.Unary.Any as Any
-  using (Any; index; map; here; there)
+  using (Any; map; here; there)
 open import Data.Product.Base as Product using (∃; _×_; _,_)
 open import Function.Base using (_∘_; id; flip; const)
 open import Relation.Binary.Definitions using (_Respects_)

From bff05769ba19967925bec1930a4f687d5b01f6d8 Mon Sep 17 00:00:00 2001
From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Date: Fri, 22 Mar 2024 15:56:45 +0000
Subject: [PATCH 21/47] Update Setoid.agda

Removed more redundant `import`ed operations
---
 src/Data/List/Membership/Setoid.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Data/List/Membership/Setoid.agda b/src/Data/List/Membership/Setoid.agda
index a88f242b20..a98c2d39a8 100644
--- a/src/Data/List/Membership/Setoid.agda
+++ b/src/Data/List/Membership/Setoid.agda
@@ -10,11 +10,11 @@ open import Relation.Binary.Bundles using (Setoid)
 
 module Data.List.Membership.Setoid {c ℓ} (S : Setoid c ℓ) where
 
-open import Data.List.Base using (List; []; _∷_; length; lookup)
+open import Data.List.Base using (List; []; _∷_)
 open import Data.List.Relation.Unary.Any as Any
   using (Any; map; here; there)
 open import Data.Product.Base as Product using (∃; _×_; _,_)
-open import Function.Base using (_∘_; id; flip; const)
+open import Function.Base using (_∘_; flip; const)
 open import Relation.Binary.Definitions using (_Respects_)
 open import Relation.Nullary.Negation using (¬_)
 open import Relation.Unary using (Pred)

From 52e8f92de0bc81bf2634c9a0aa2f4a13919e7856 Mon Sep 17 00:00:00 2001
From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Date: Fri, 22 Mar 2024 16:04:37 +0000
Subject: [PATCH 22/47] Update Properties.agda

Another redundant `import`
---
 src/Data/List/Membership/Propositional/Properties.agda | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/Data/List/Membership/Propositional/Properties.agda b/src/Data/List/Membership/Propositional/Properties.agda
index 40f4792230..fe5cba2657 100644
--- a/src/Data/List/Membership/Propositional/Properties.agda
+++ b/src/Data/List/Membership/Propositional/Properties.agda
@@ -9,7 +9,6 @@
 module Data.List.Membership.Propositional.Properties where
 
 open import Algebra using (Op₂; Selective)
-open import Data.Bool.Base using (Bool; false; true; if_then_else_)
 open import Data.Fin.Base using (Fin)
 open import Data.List.Base as List
 open import Data.List.Effectful using (monad)

From a3d3c7ea7346630fd731282dbd0be203153d1c9c Mon Sep 17 00:00:00 2001
From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Date: Fri, 22 Mar 2024 17:02:27 +0000
Subject: [PATCH 23/47] Update Properties.agda

Another redundant `import`ed operation
---
 src/Data/List/Membership/Propositional/Properties.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/List/Membership/Propositional/Properties.agda b/src/Data/List/Membership/Propositional/Properties.agda
index fe5cba2657..5903ff8703 100644
--- a/src/Data/List/Membership/Propositional/Properties.agda
+++ b/src/Data/List/Membership/Propositional/Properties.agda
@@ -39,7 +39,7 @@ open import Relation.Binary.Definitions as Binary hiding (Decidable)
 open import Relation.Binary.PropositionalEquality as ≡
   using (_≡_; _≢_; refl; sym; trans; cong; resp; →-to-⟶; _≗_)
 import Relation.Binary.Properties.DecTotalOrder as DTOProperties
-open import Relation.Nullary.Decidable using (Dec; does; yes; no; ¬¬-excluded-middle)
+open import Relation.Nullary.Decidable using (Dec; yes; no; ¬¬-excluded-middle)
 open import Relation.Nullary.Negation using (¬_; contradiction)
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Unary using (_⟨×⟩_; Decidable)

From 644ee074e7d4dab726abff5ba7ca0e23ee3d9285 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 23 Mar 2024 18:14:10 +0000
Subject: [PATCH 24/47] `with` into `let`

---
 src/Data/List/Membership/Propositional/Properties.agda | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Data/List/Membership/Propositional/Properties.agda b/src/Data/List/Membership/Propositional/Properties.agda
index 5903ff8703..de67fa4a1d 100644
--- a/src/Data/List/Membership/Propositional/Properties.agda
+++ b/src/Data/List/Membership/Propositional/Properties.agda
@@ -142,9 +142,9 @@ module _ {v : A} where
     Membership.∈-concat⁺′ (≡.setoid A) v∈vs (Any.map ≡⇒≋ vs∈xss)
 
   ∈-concat⁻′ : ∀ xss → v ∈ concat xss → ∃ λ xs → v ∈ xs × xs ∈ xss
-  ∈-concat⁻′ xss v∈c
-    with xs , v∈xs , xs∈xss ← Membership.∈-concat⁻′ (≡.setoid A) xss v∈c
-    = xs , v∈xs , Any.map ≋⇒≡ xs∈xss
+  ∈-concat⁻′ xss v∈c =
+    let xs , v∈xs , xs∈xss = Membership.∈-concat⁻′ (≡.setoid A) xss v∈c
+    in xs , v∈xs , Any.map ≋⇒≡ xs∈xss
 
   concat-∈↔ : ∀ {xss : List (List A)} →
               (∃ λ xs → v ∈ xs × xs ∈ xss) ↔ v ∈ concat xss

From 78382c5d783dc66a08f8f4a174f7fd7b752ba334 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 23 Mar 2024 18:20:53 +0000
Subject: [PATCH 25/47] `with` into `let`

---
 .../List/Membership/Setoid/Properties.agda     | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

diff --git a/src/Data/List/Membership/Setoid/Properties.agda b/src/Data/List/Membership/Setoid/Properties.agda
index 3e6942f5cb..a28d85bfc0 100644
--- a/src/Data/List/Membership/Setoid/Properties.agda
+++ b/src/Data/List/Membership/Setoid/Properties.agda
@@ -211,8 +211,8 @@ module _ (S : Setoid c ℓ) where
   ∈-∃++ : ∀ {v xs} → v ∈ xs → ∃₂ λ ys zs → ∃ λ w →
           v ≈ w × xs ≋ ys ++ [ w ] ++ zs
   ∈-∃++ (here px)        = [] , _ , _ , px , ≋-refl
-  ∈-∃++ (there {d} v∈xs) with hs , _ , _ , v≈v′ , eq ← ∈-∃++ v∈xs
-                         = d ∷ hs , _ , _ , v≈v′ , refl ∷ eq
+  ∈-∃++ (there {d} v∈xs) = let hs , _ , _ , v≈v′ , eq = ∈-∃++ v∈xs
+                           in d ∷ hs , _ , _ , v≈v′ , refl ∷ eq
 
 ------------------------------------------------------------------------
 -- concat
@@ -234,8 +234,8 @@ module _ (S : Setoid c ℓ) where
   ∈-concat⁺′ v∈vs = ∈-concat⁺ ∘ Any.map (flip (∈-resp-≋ S) v∈vs)
 
   ∈-concat⁻′ : ∀ {v} xss → v ∈ concat xss → ∃ λ xs → v ∈ xs × xs ∈ₗ xss
-  ∈-concat⁻′ xss v∈c[xss]
-    with xs , xs∈xss , v∈xs ← find (∈-concat⁻ xss v∈c[xss]) = xs , v∈xs , xs∈xss
+  ∈-concat⁻′ xss v∈c[xss] =
+    let xs , xs∈xss , v∈xs = find (∈-concat⁻ xss v∈c[xss]) in xs , v∈xs , xs∈xss
 
 ------------------------------------------------------------------------
 -- cartesianProductWith
@@ -257,10 +257,12 @@ module _ (S₁ : Setoid c₁ ℓ₁) (S₂ : Setoid c₂ ℓ₂) (S₃ : Setoid
   ∈-cartesianProductWith⁻ : ∀ f xs ys {v} → v ∈₃ cartesianProductWith f xs ys →
                             ∃₂ λ a b → a ∈₁ xs × b ∈₂ ys × v ≈₃ f a b
   ∈-cartesianProductWith⁻ f (x ∷ xs) ys v∈c with ∈-++⁻ S₃ (map (f x) ys) v∈c
-  ∈-cartesianProductWith⁻ f (x ∷ xs) ys v∈c | inj₁ v∈map with ∈-map⁻ S₂ S₃ v∈map
-  ... | (b , b∈ys , v≈fxb) = x , b , here refl₁ , b∈ys , v≈fxb
-  ∈-cartesianProductWith⁻ f (x ∷ xs) ys v∈c | inj₂ v∈com with ∈-cartesianProductWith⁻ f xs ys v∈com
-  ... | (a , b , a∈xs , b∈ys , v≈fab) = a , b , there a∈xs , b∈ys , v≈fab
+  ... | inj₁ v∈map =
+    let b , b∈ys , v≈fxb = ∈-map⁻ S₂ S₃ v∈map
+    in x , b , here refl₁ , b∈ys , v≈fxb
+  ... | inj₂ v∈com =
+    let a , b , a∈xs , b∈ys , v≈fab = ∈-cartesianProductWith⁻ f xs ys v∈com
+    in  a , b , there a∈xs , b∈ys , v≈fab
 
 ------------------------------------------------------------------------
 -- cartesianProduct

From 07236c7e9550000bfe4918eff8584df52fcffb1e Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 23 Mar 2024 18:26:37 +0000
Subject: [PATCH 26/47] `with` into `let`

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

diff --git a/src/Data/List/Relation/Unary/All/Properties.agda b/src/Data/List/Relation/Unary/All/Properties.agda
index fee1579193..9a469a6146 100644
--- a/src/Data/List/Relation/Unary/All/Properties.agda
+++ b/src/Data/List/Relation/Unary/All/Properties.agda
@@ -386,8 +386,7 @@ mapMaybe⁺ : ∀ {f : A → Maybe B} →
 mapMaybe⁺ {xs = []}     {f = f} []         = []
 mapMaybe⁺ {xs = x ∷ xs} {f = f} (px ∷ pxs) with f x
 ... | nothing = mapMaybe⁺ pxs
-... | just v with px
-...   | just pv = pv ∷ mapMaybe⁺ pxs
+... | just v with just pv ← px = pv ∷ mapMaybe⁺ pxs
 
 ------------------------------------------------------------------------
 -- catMaybes
@@ -720,8 +719,9 @@ module _ (p : A → Bool) where
 
   all⁺ : ∀ xs → T (all p xs) → All (T ∘ p) xs
   all⁺ []       _      = []
-  all⁺ (x ∷ xs) px∷pxs
-    with px , pxs ← Equivalence.to (T-∧ {p x}) px∷pxs = px ∷ all⁺ xs pxs
+  all⁺ (x ∷ xs) px∷pxs =
+    let px , pxs = Equivalence.to (T-∧ {p x}) px∷pxs
+    in px ∷ all⁺ xs pxs
 
   all⁻ : All (T ∘ p) xs → T (all p xs)
   all⁻ []         = _

From 3e1c687dfa8bafe8a7efdf637a7f631304cc926a Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 23 Mar 2024 18:39:12 +0000
Subject: [PATCH 27/47] `with` into `let`

---
 .../List/Relation/Unary/Any/Properties.agda   | 23 ++++++++++---------
 1 file changed, 12 insertions(+), 11 deletions(-)

diff --git a/src/Data/List/Relation/Unary/Any/Properties.agda b/src/Data/List/Relation/Unary/Any/Properties.agda
index 9b85d362e6..6acef67a24 100644
--- a/src/Data/List/Relation/Unary/Any/Properties.agda
+++ b/src/Data/List/Relation/Unary/Any/Properties.agda
@@ -485,10 +485,10 @@ module _ (f : A → B → C) where
                           Any R (cartesianProductWith f xs ys) →
                           Any P xs × Any Q ys
   cartesianProductWith⁻ resp (x ∷ xs) ys Rxsys with ++⁻ (map (f x) ys) Rxsys
-  cartesianProductWith⁻ resp (x ∷ xs) ys Rxsys | inj₁ Rfxys with map⁻ Rfxys
-  ... | Rxys = here (proj₁ (resp (proj₂ (Any.satisfied Rxys)))) , Any.map (proj₂ ∘ resp) Rxys
-  cartesianProductWith⁻ resp (x ∷ xs) ys Rxsys | inj₂ Rc with cartesianProductWith⁻ resp xs ys Rc
-  ... | pxs , qys = there pxs , qys
+  ... | inj₁ Rfxys = let Rxys = map⁻ Rfxys
+    in here (proj₁ (resp (proj₂ (Any.satisfied Rxys)))) , Any.map (proj₂ ∘ resp) Rxys
+  ... | inj₂ Rc    = let pxs , qys = cartesianProductWith⁻ resp xs ys Rc
+    in there pxs , qys
 
 ------------------------------------------------------------------------
 -- cartesianProduct
@@ -512,8 +512,8 @@ applyUpTo⁺ f p (s<s i<n@(s≤s _)) =
 applyUpTo⁻ : ∀ f {n} → Any P (applyUpTo f n) →
              ∃ λ i → i < n × P (f i)
 applyUpTo⁻ f {suc n} (here p)  = zero , z<s , p
-applyUpTo⁻ f {suc n} (there p)
-  with i , i<n , q ← applyUpTo⁻ (f ∘ suc) p = suc i , s<s i<n , q
+applyUpTo⁻ f {suc n} (there p) =
+  let i , i<n , q = applyUpTo⁻ (f ∘ suc) p in suc i , s<s i<n , q
 
 ------------------------------------------------------------------------
 -- applyDownFrom
@@ -526,8 +526,8 @@ applyDownFrom⁺ f {i} {suc n} p (s≤s i≤n) with i ≟ n
 applyDownFrom⁻ : ∀ f {n} → Any P (applyDownFrom f n) →
                  ∃ λ i → i < n × P (f i)
 applyDownFrom⁻ f {suc n} (here p)  = n , ≤-refl , p
-applyDownFrom⁻ f {suc n} (there p)
-  with i , i<n , q ← applyDownFrom⁻ f p = i , m<n⇒m<1+n i<n , q
+applyDownFrom⁻ f {suc n} (there p) =
+  let i , i<n , q = applyDownFrom⁻ f p in i , m<n⇒m<1+n i<n , q
 
 ------------------------------------------------------------------------
 -- tabulate
@@ -581,9 +581,10 @@ module _ {R : Rel A r} (R? : B.Decidable R) where
   deduplicate⁺ {xs = x ∷ xs} resp (here px)   = here px
   deduplicate⁺ {xs = x ∷ xs} resp (there pxs)
     with filter⁺ (¬? ∘ R? x) (deduplicate⁺ resp pxs)
-  ... | inj₁ p = there p
-  ... | inj₂ ¬¬q with decidable-stable (R? x (Any.lookup (deduplicate⁺ resp pxs))) ¬¬q
-  ...  | q = here (resp q (lookup-result (deduplicate⁺ resp pxs)))
+  ... | inj₁ p   = there p
+  ... | inj₂ ¬¬q =
+    let q = decidable-stable (R? x (Any.lookup (deduplicate⁺ resp pxs))) ¬¬q
+    in  here (resp q (lookup-result (deduplicate⁺ resp pxs)))
 
   private
     derun⁻-aux : Any P (derun R? (x ∷ xs)) → Any P (x ∷ xs)

From 66a6207a14332f7e3ff15d9e15dc196159f5ace8 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 24 Mar 2024 10:15:16 +0000
Subject: [PATCH 28/47] indentation

---
 src/Data/List/Membership/Setoid/Properties.agda | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/Data/List/Membership/Setoid/Properties.agda b/src/Data/List/Membership/Setoid/Properties.agda
index a28d85bfc0..7dd39fe6b0 100644
--- a/src/Data/List/Membership/Setoid/Properties.agda
+++ b/src/Data/List/Membership/Setoid/Properties.agda
@@ -211,8 +211,9 @@ module _ (S : Setoid c ℓ) where
   ∈-∃++ : ∀ {v xs} → v ∈ xs → ∃₂ λ ys zs → ∃ λ w →
           v ≈ w × xs ≋ ys ++ [ w ] ++ zs
   ∈-∃++ (here px)        = [] , _ , _ , px , ≋-refl
-  ∈-∃++ (there {d} v∈xs) = let hs , _ , _ , v≈v′ , eq = ∈-∃++ v∈xs
-                           in d ∷ hs , _ , _ , v≈v′ , refl ∷ eq
+  ∈-∃++ (there {d} v∈xs) =
+    let hs , _ , _ , v≈v′ , eq = ∈-∃++ v∈xs
+    in d ∷ hs , _ , _ , v≈v′ , refl ∷ eq
 
 ------------------------------------------------------------------------
 -- concat

From 05a5176b63c1ab8dc85c24794e42074f9856d628 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 24 Mar 2024 10:17:31 +0000
Subject: [PATCH 29/47] fix `universal-U`

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

diff --git a/src/Data/List/Relation/Unary/All.agda b/src/Data/List/Relation/Unary/All.agda
index 16a7be9d69..f70e1dc1f7 100644
--- a/src/Data/List/Relation/Unary/All.agda
+++ b/src/Data/List/Relation/Unary/All.agda
@@ -212,7 +212,7 @@ universal : Universal P → Universal (All P)
 universal u []       = []
 universal u (x ∷ xs) = u x ∷ universal u xs
 
-universal-U : Universal (All (U {A = A}))
+universal-U : Universal (All {A = A} U)
 universal-U = universal Unary.U-Universal
 
 irrelevant : Irrelevant P → Irrelevant (All P)

From 9549a9ed6ff6d5a185dd7bfda0b169dbfe7ef0ed Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 24 Mar 2024 11:34:03 +0000
Subject: [PATCH 30/47] added `map-cong`

---
 CHANGELOG.md                                     | 6 ++++++
 src/Data/List/Relation/Unary/Any/Properties.agda | 7 +++----
 2 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index eec3f40cab..e223b08349 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -275,6 +275,12 @@ Additions to existing modules
   tabulate⁺-< : (i < j → R (f i) (f j)) → AllPairs R (tabulate f)
   ```
 
+* In `Data.List.Relation.Unary.Any.Properties`:
+  ```agda
+  map-cong : (f g : P ⋐ Q) → (∀ {x} (p : P x) → f p ≡ g p) →
+             (p : Any P xs) → Any.map f p ≡ Any.map g p
+  ```
+
 * In `Data.List.Relation.Ternary.Appending.Setoid.Properties`:
   ```agda
   through→ : ∃[ xs ] Pointwise _≈_ as xs × Appending xs bs cs →
diff --git a/src/Data/List/Relation/Unary/Any/Properties.agda b/src/Data/List/Relation/Unary/Any/Properties.agda
index 6acef67a24..d0e1369755 100644
--- a/src/Data/List/Relation/Unary/Any/Properties.agda
+++ b/src/Data/List/Relation/Unary/Any/Properties.agda
@@ -26,7 +26,6 @@ open import Data.Maybe.Base using (Maybe; just; nothing)
 open import Data.Maybe.Relation.Unary.Any as MAny using (just)
 open import Data.Product.Base as Product
   using (_×_; _,_; ∃; ∃₂; proj₁; proj₂)
-open import Data.Product.Properties
 open import Data.Product.Function.NonDependent.Propositional
   using (_×-cong_)
 import Data.Product.Function.Dependent.Propositional as Σ
@@ -97,10 +96,10 @@ Any-cong {P = P} {Q = Q} {xs = xs} {ys} P↔Q xs≈ys =
 ------------------------------------------------------------------------
 -- Any.map
 
-map-ext : (f g : P ⋐ P) → (∀ {x} (p : P x) → f p ≡ g p) →
+map-cong : (f g : P ⋐ Q) → (∀ {x} (p : P x) → f p ≡ g p) →
           (p : Any P xs) → Any.map f p ≡ Any.map g p
-map-ext f g hyp (here  p) = cong here (hyp p)
-map-ext f g hyp (there p) = cong there $ map-ext f g hyp p
+map-cong f g hyp (here  p) = cong here (hyp p)
+map-cong f g hyp (there p) = cong there $ map-cong f g hyp p
 
 map-id : ∀ (f : P ⋐ P) → (∀ {x} (p : P x) → f p ≡ p) →
          (p : Any P xs) → Any.map f p ≡ p

From 8ad545b0e00d6ed468b388a8a7f92bfcc46be172 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 24 Mar 2024 11:37:17 +0000
Subject: [PATCH 31/47] =?UTF-8?q?deprecate=20`map-compose`=20in=20favour?=
 =?UTF-8?q?=20of=20`map-=E2=88=98`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 CHANGELOG.md                                  |  7 +++++-
 .../List/Relation/Unary/All/Properties.agda   | 24 ++++++++++++-------
 2 files changed, 22 insertions(+), 9 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index e223b08349..301c33d08e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -46,6 +46,11 @@ Deprecated names
   _-_  ↦  _//_
   ```
 
+* In `Data.List.Relation.Unary.All.Properties`:
+  ```agda
+  map-compose  ↦  map-∘
+  ```
+
 * In `Data.Nat.Divisibility.Core`:
   ```agda
   *-pres-∣  ↦  Data.Nat.Divisibility.*-pres-∣
@@ -408,4 +413,4 @@ Additions to existing modules
   ```
 
 * `Tactic.Cong` now provides a marker function, `⌞_⌟`, for user-guided
-  anti-unification. See README.Tactic.Cong for details.
+  anti-unification. See `README.Tactic.Cong` for details.
diff --git a/src/Data/List/Relation/Unary/All/Properties.agda b/src/Data/List/Relation/Unary/All/Properties.agda
index 9a469a6146..79226f46eb 100644
--- a/src/Data/List/Relation/Unary/All/Properties.agda
+++ b/src/Data/List/Relation/Unary/All/Properties.agda
@@ -176,19 +176,19 @@ lookup⇒[]= pxs i refl = []=lookup pxs i
 ------------------------------------------------------------------------
 -- map
 
-map-id : ∀ (pxs : All P xs) → All.map id pxs ≡ pxs
-map-id []         = refl
-map-id (px ∷ pxs) = cong (px ∷_)  (map-id pxs)
-
 map-cong : ∀ {f : P ⋐ Q} {g : P ⋐ Q} (pxs : All P xs) →
            (∀ {x} → f {x} ≗ g) → All.map f pxs ≡ All.map g pxs
 map-cong []         _   = refl
 map-cong (px ∷ pxs) feq = cong₂ _∷_ (feq px) (map-cong pxs feq)
 
-map-compose : ∀ {f : P ⋐ Q} {g : Q ⋐ R} (pxs : All P xs) →
-              All.map g (All.map f pxs) ≡ All.map (g ∘ f) pxs
-map-compose []         = refl
-map-compose (px ∷ pxs) = cong (_ ∷_) (map-compose pxs)
+map-id : ∀ (pxs : All P xs) → All.map id pxs ≡ pxs
+map-id []         = refl
+map-id (px ∷ pxs) = cong (px ∷_)  (map-id pxs)
+
+map-∘ : ∀ {f : P ⋐ Q} {g : Q ⋐ R} (pxs : All P xs) →
+        All.map g (All.map f pxs) ≡ All.map (g ∘ f) pxs
+map-∘ []         = refl
+map-∘ (px ∷ pxs) = cong (_ ∷_) (map-∘ pxs)
 
 lookup-map : ∀ {f : P ⋐ Q} (pxs : All P xs) (i : x ∈ xs) →
              lookup (All.map f pxs) i ≡ f (lookup pxs i)
@@ -794,3 +794,11 @@ gmap = gmap⁺
 "Warning: gmap was deprecated in v2.0.
 Please use gmap⁺ instead."
 #-}
+
+-- Version 2.1
+
+map-compose = map-∘
+{-# WARNING_ON_USAGE map-compose
+"Warning: map-compose was deprecated in v2.1.
+Please use map-∘ instead."
+#-}

From 029305c33b303189885f7de7f8a6a98b3a956c67 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 24 Mar 2024 12:11:44 +0000
Subject: [PATCH 32/47] =?UTF-8?q?explicit=20`let`=20in=20statement=20of=20?=
 =?UTF-8?q?`find=E2=88=98map`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Data/List/Membership/Propositional/Properties/Core.agda | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Data/List/Membership/Propositional/Properties/Core.agda b/src/Data/List/Membership/Propositional/Properties/Core.agda
index 9273630b4f..25693e8a81 100644
--- a/src/Data/List/Membership/Propositional/Properties/Core.agda
+++ b/src/Data/List/Membership/Propositional/Properties/Core.agda
@@ -50,7 +50,8 @@ module _ {P : Pred A p} where
   map∘find (there p) hyp = cong there (map∘find p hyp)
 
   find∘map : ∀ {Q : Pred A q} {xs} (p : Any P xs) (f : P ⊆ Q) →
-             find (Any.map f p) ≡ Product.map id (Product.map id f) (find p)
+             let x , x∈xs , px = find p in
+             find (Any.map f p) ≡ (x , x∈xs , f px)
   find∘map (here  p) f = refl
   find∘map (there p) f rewrite find∘map p f = refl
 

From ccc00eeb09fefef511846698c643bd4334a1e2e6 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 24 Mar 2024 12:42:04 +0000
Subject: [PATCH 33/47] knock-on viscosity: hide `map-cong`

---
 src/Data/List/Relation/Binary/BagAndSetEquality.agda | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Data/List/Relation/Binary/BagAndSetEquality.agda b/src/Data/List/Relation/Binary/BagAndSetEquality.agda
index f014df8b41..74fc51c974 100644
--- a/src/Data/List/Relation/Binary/BagAndSetEquality.agda
+++ b/src/Data/List/Relation/Binary/BagAndSetEquality.agda
@@ -17,14 +17,14 @@ open import Data.List.Base
 open import Data.List.Effectful using (monad; module Applicative; module MonadProperties)
 import Data.List.Properties as List
 open import Data.List.Relation.Unary.Any using (Any; here; there)
-open import Data.List.Relation.Unary.Any.Properties hiding (++-comm)
+open import Data.List.Relation.Unary.Any.Properties hiding (map-cong; ++-comm)
 open import Data.List.Membership.Propositional using (_∈_)
 open import Data.List.Membership.Propositional.Properties
 open import Data.List.Relation.Binary.Subset.Propositional.Properties
   using (⊆-preorder)
 open import Data.List.Relation.Binary.Permutation.Propositional
 open import Data.List.Relation.Binary.Permutation.Propositional.Properties
-open import Data.Product.Base as Prod hiding (map)
+open import Data.Product.Base as Product hiding (map)
 import Data.Product.Function.Dependent.Propositional as Σ
 open import Data.Sum.Base as Sum hiding (map)
 open import Data.Sum.Properties hiding (map-cong)
@@ -388,10 +388,10 @@ drop-cons {x = x} {xs} {ys} x∷xs≈x∷ys =
     index-of (to xs≈ys (proj₂
       (from (Fin-length xs) (to (Fin-length xs) (z , p)))))   ≡⟨⟩
 
-    index-of (proj₂ (Prod.map id (to xs≈ys)
+    index-of (proj₂ (Product.map id (to xs≈ys)
       (from (Fin-length xs) (to (Fin-length xs) (z , p)))))  ≡⟨⟩
 
-    to (Fin-length ys) (Prod.map id (to xs≈ys)
+    to (Fin-length ys) (Product.map id (to xs≈ys)
       (from (Fin-length xs) (index-of p)))                          ≡⟨⟩
 
     to (Fin-length-cong xs≈ys) (index-of p)                        ∎

From c5dd3fc251d20b761dff7ab8348b1bcc96d3076c Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 24 Mar 2024 18:31:23 +0000
Subject: [PATCH 34/47] =?UTF-8?q?use=20of=20`Product.map=E2=82=81`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Data/List/Relation/Binary/BagAndSetEquality.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/List/Relation/Binary/BagAndSetEquality.agda b/src/Data/List/Relation/Binary/BagAndSetEquality.agda
index 74fc51c974..e671a1f70e 100644
--- a/src/Data/List/Relation/Binary/BagAndSetEquality.agda
+++ b/src/Data/List/Relation/Binary/BagAndSetEquality.agda
@@ -388,7 +388,7 @@ drop-cons {x = x} {xs} {ys} x∷xs≈x∷ys =
     index-of (to xs≈ys (proj₂
       (from (Fin-length xs) (to (Fin-length xs) (z , p)))))   ≡⟨⟩
 
-    index-of (proj₂ (Product.map id (to xs≈ys)
+    index-of (proj₂ (Product.map₁ (to xs≈ys)
       (from (Fin-length xs) (to (Fin-length xs) (z , p)))))  ≡⟨⟩
 
     to (Fin-length ys) (Product.map id (to xs≈ys)

From 8149f20bab39ec9a71e8c9f787820e8d50995b31 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 24 Mar 2024 18:40:08 +0000
Subject: [PATCH 35/47] =?UTF-8?q?revert=20use=20of=20`Product.map=E2=82=81?=
 =?UTF-8?q?`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Data/List/Relation/Binary/BagAndSetEquality.agda | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Data/List/Relation/Binary/BagAndSetEquality.agda b/src/Data/List/Relation/Binary/BagAndSetEquality.agda
index e671a1f70e..575ca40fcd 100644
--- a/src/Data/List/Relation/Binary/BagAndSetEquality.agda
+++ b/src/Data/List/Relation/Binary/BagAndSetEquality.agda
@@ -388,13 +388,13 @@ drop-cons {x = x} {xs} {ys} x∷xs≈x∷ys =
     index-of (to xs≈ys (proj₂
       (from (Fin-length xs) (to (Fin-length xs) (z , p)))))   ≡⟨⟩
 
-    index-of (proj₂ (Product.map₁ (to xs≈ys)
-      (from (Fin-length xs) (to (Fin-length xs) (z , p)))))  ≡⟨⟩
+    index-of (proj₂ (Product.map id (to xs≈ys)
+      (from (Fin-length xs) (to (Fin-length xs) (z , p)))))   ≡⟨⟩
 
     to (Fin-length ys) (Product.map id (to xs≈ys)
-      (from (Fin-length xs) (index-of p)))                          ≡⟨⟩
+      (from (Fin-length xs) (index-of p)))                    ≡⟨⟩
 
-    to (Fin-length-cong xs≈ys) (index-of p)                        ∎
+    to (Fin-length-cong xs≈ys) (index-of p)                   ∎
     where
     open ≡-Reasoning
     open Inverse

From d25c9697fad7e07f91c6579e6f4bf4a3ed3fd3aa Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 24 Mar 2024 19:35:47 +0000
Subject: [PATCH 36/47] inlined lemmas!

---
 src/Data/List/Relation/Unary/Any/Properties.agda | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/Data/List/Relation/Unary/Any/Properties.agda b/src/Data/List/Relation/Unary/Any/Properties.agda
index d0e1369755..a538f56ce0 100644
--- a/src/Data/List/Relation/Unary/Any/Properties.agda
+++ b/src/Data/List/Relation/Unary/Any/Properties.agda
@@ -265,23 +265,23 @@ Any-×⁻ pq = let x , x∈xs , pq′ = find pq in
   to∘from : ∀ pq → Any-×⁺ (Any-×⁻ pq) ≡ pq
   to∘from pq =
     let x , x∈xs , pq′ = find pq
-
+{-
         lem₁ : {f : (x ≡_) ⋐ λ x → Any (λ y → (P x) × (Q y)) ys} →
                (f-refl : f refl ≡ pq′) → Any.map f _ ≡ pq
         lem₁ {f} = map∘find pq {f = f}
-
+-}
         y , y∈ys , p , q = find pq′
-
+{-
         lem₂ : {g : (y ≡_) ⋐ λ y → (P x) × (Q y)} →
                (g-refl : g refl ≡ (p , q)) → Any.map g _ ≡ pq′
         lem₂ {g} = map∘find pq′ {f = g}
-
+-}
         helper : Any.map (p ,_) (lose y∈ys q) ≡ pq′
         helper = begin
           Any.map (p ,_) (lose y∈ys q)
             ≡⟨ map-∘ (p ,_) (λ z → resp Q z q) y∈ys ⟨
           Any.map (λ z → p , resp Q z q) y∈ys
-            ≡⟨ lem₂ refl ⟩
+            ≡⟨ map∘find pq′ refl ⟩
           pq′
             ∎
 
@@ -294,7 +294,7 @@ Any-×⁻ pq = let x , x∈xs , pq′ = find pq in
       Any.map h (lose x∈xs p)
         ≡⟨ map-∘ h (λ z → resp P z p) x∈xs ⟨
       Any.map (λ z → Any.map (resp P z p ,_) (lose y∈ys q)) x∈xs
-        ≡⟨ lem₁ helper ⟩
+        ≡⟨ map∘find pq helper ⟩
       pq
         ∎
 

From fb0307dc7b765e5c73b2a85b546b0a42eda1aa19 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 25 Mar 2024 07:24:18 +0000
Subject: [PATCH 37/47] alpha conversion and further inlining!

---
 .../List/Relation/Unary/Any/Properties.agda   | 33 +++++++------------
 1 file changed, 12 insertions(+), 21 deletions(-)

diff --git a/src/Data/List/Relation/Unary/Any/Properties.agda b/src/Data/List/Relation/Unary/Any/Properties.agda
index a538f56ce0..7b521de31f 100644
--- a/src/Data/List/Relation/Unary/Any/Properties.agda
+++ b/src/Data/List/Relation/Unary/Any/Properties.agda
@@ -265,35 +265,26 @@ Any-×⁻ pq = let x , x∈xs , pq′ = find pq in
   to∘from : ∀ pq → Any-×⁺ (Any-×⁻ pq) ≡ pq
   to∘from pq =
     let x , x∈xs , pq′ = find pq
-{-
-        lem₁ : {f : (x ≡_) ⋐ λ x → Any (λ y → (P x) × (Q y)) ys} →
-               (f-refl : f refl ≡ pq′) → Any.map f _ ≡ pq
-        lem₁ {f} = map∘find pq {f = f}
--}
-        y , y∈ys , p , q = find pq′
-{-
-        lem₂ : {g : (y ≡_) ⋐ λ y → (P x) × (Q y)} →
-               (g-refl : g refl ≡ (p , q)) → Any.map g _ ≡ pq′
-        lem₂ {g} = map∘find pq′ {f = g}
--}
-        helper : Any.map (p ,_) (lose y∈ys q) ≡ pq′
+        y , y∈ys , px , qy = find pq′
+
+        h : P ⋐ λ x → Any (λ y → (P x) × (Q y)) ys
+        h p = Any.map (p ,_) (lose y∈ys qy)
+
+        helper : h px ≡ pq′
         helper = begin
-          Any.map (p ,_) (lose y∈ys q)
-            ≡⟨ map-∘ (p ,_) (λ z → resp Q z q) y∈ys ⟨
-          Any.map (λ z → p , resp Q z q) y∈ys
+          Any.map (px ,_) (lose y∈ys qy)
+            ≡⟨ map-∘ (px ,_) (λ z → resp Q z qy) y∈ys ⟨
+          Any.map (λ z → px , resp Q z qy) y∈ys
             ≡⟨ map∘find pq′ refl ⟩
           pq′
             ∎
 
-        h : P ⋐ λ x → Any (λ y → (P x) × (Q y)) ys
-        h p = Any.map (p ,_) (lose y∈ys q)
-
     in  begin
       Any-×⁺ (Any-×⁻ pq)
         ≡⟨⟩
-      Any.map h (lose x∈xs p)
-        ≡⟨ map-∘ h (λ z → resp P z p) x∈xs ⟨
-      Any.map (λ z → Any.map (resp P z p ,_) (lose y∈ys q)) x∈xs
+      Any.map h (lose x∈xs px)
+        ≡⟨ map-∘ h (λ z → resp P z px) x∈xs ⟨
+      Any.map (λ z → Any.map (resp P z px ,_) (lose y∈ys qy)) x∈xs
         ≡⟨ map∘find pq helper ⟩
       pq
         ∎

From 04a6d0d04ed6494dd768271b86f801ed22dcd4db Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 25 Mar 2024 07:29:15 +0000
Subject: [PATCH 38/47] =?UTF-8?q?correctted=20use=20of=20`Product.map?=
 =?UTF-8?q?=E2=82=82`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Data/List/Relation/Binary/BagAndSetEquality.agda | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/Data/List/Relation/Binary/BagAndSetEquality.agda b/src/Data/List/Relation/Binary/BagAndSetEquality.agda
index 575ca40fcd..127e58d30a 100644
--- a/src/Data/List/Relation/Binary/BagAndSetEquality.agda
+++ b/src/Data/List/Relation/Binary/BagAndSetEquality.agda
@@ -388,10 +388,10 @@ drop-cons {x = x} {xs} {ys} x∷xs≈x∷ys =
     index-of (to xs≈ys (proj₂
       (from (Fin-length xs) (to (Fin-length xs) (z , p)))))   ≡⟨⟩
 
-    index-of (proj₂ (Product.map id (to xs≈ys)
+    index-of (proj₂ (Product.map₂ (to xs≈ys)
       (from (Fin-length xs) (to (Fin-length xs) (z , p)))))   ≡⟨⟩
 
-    to (Fin-length ys) (Product.map id (to xs≈ys)
+    to (Fin-length ys) (Product.map₂ (to xs≈ys)
       (from (Fin-length xs) (index-of p)))                    ≡⟨⟩
 
     to (Fin-length-cong xs≈ys) (index-of p)                   ∎
@@ -421,10 +421,10 @@ drop-cons {x = x} {xs} {ys} x∷xs≈x∷ys =
     index-of (Inverse.to xs≈ys p) ≡
     index-of (Inverse.to xs≈ys q)
   index-equality-preserved {p = p} {q} xs≈ys eq =
-    index-of (Inverse.to xs≈ys p)                  ≡⟨ index-of-commutes xs≈ys p ⟩
-    Inverse.to (Fin-length-cong xs≈ys) (index-of p)  ≡⟨ ≡.cong (Inverse.to (Fin-length-cong xs≈ys)) eq ⟩
-    Inverse.to (Fin-length-cong xs≈ys) (index-of q)  ≡⟨ ≡.sym $ index-of-commutes xs≈ys q ⟩
-    index-of (Inverse.to xs≈ys q)                  ∎
+    index-of (Inverse.to xs≈ys p)                   ≡⟨ index-of-commutes xs≈ys p ⟩
+    Inverse.to (Fin-length-cong xs≈ys) (index-of p) ≡⟨ ≡.cong (Inverse.to (Fin-length-cong xs≈ys)) eq ⟩
+    Inverse.to (Fin-length-cong xs≈ys) (index-of q) ≡⟨ ≡.sym $ index-of-commutes xs≈ys q ⟩
+    index-of (Inverse.to xs≈ys q)                   ∎
     where
     open ≡-Reasoning
 

From 3a554dc0a39b78a51d809b9a71ba1cb0815c81a6 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 25 Mar 2024 12:17:42 +0000
Subject: [PATCH 39/47] added `syntax` declarations for the new combinators

---
 CHANGELOG.md                         | 13 +++++++++----
 src/Data/List/Membership/Setoid.agda | 14 ++++++++++++--
 2 files changed, 21 insertions(+), 6 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index d029c73fef..e838de7474 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -261,10 +261,15 @@ Additions to existing modules
   ∃∈-Any∘find : (p : Any P xs) → ∃∈-Any (find p) ≡ p
   ```
 
-* In `Data.List.Membership.Setoid`: two abbreviations for predicate transformers
-  ```agda
-  ∃∈ P xs = ∃ λ x → x ∈ xs × P x
-  ∀∈ P xs = ∀ {x} → x ∈ xs → P x
+* In `Data.List.Membership.Setoid`: two abbreviations for predicate transformers,
+  with associated `syntax` declarations
+  ```agda
+  ∃∈-syntax : ∀ {p} (P : Pred A p) → Pred (List A) _
+  ∃∈-syntax P xs = ∃ λ x → x ∈ xs × P x
+  ∀∈-syntax : ∀ {p} (P : Pred A p) → Pred (List A) _
+  ∀∈-syntax P xs = ∀ {x} → x ∈ xs → P x
+  syntax ∃∈-syntax (λ x → P) xs = ∃[ x ∈ xs ] P
+  syntax ∀∈-syntax (λ x → P) xs = ∀[ x ∈ xs ] P
   ```
 
 * In `Data.List.Properties`:
diff --git a/src/Data/List/Membership/Setoid.agda b/src/Data/List/Membership/Setoid.agda
index a98c2d39a8..500d55a9c9 100644
--- a/src/Data/List/Membership/Setoid.agda
+++ b/src/Data/List/Membership/Setoid.agda
@@ -35,9 +35,19 @@ x ∉ xs = ¬ x ∈ xs
 ∃∈ : ∀ {p} (P : Pred A p) → Pred (List A) _
 ∃∈ P xs = ∃ λ x → x ∈ xs × P x
 
+∃∈-syntax : ∀ {p} (P : Pred A p) → Pred (List A) _
+∃∈-syntax = ∃∈
+
+syntax ∃∈-syntax (λ x → P) xs = ∃[ x ∈ xs ] P
+
 ∀∈ : ∀ {p} (P : Pred A p) → Pred (List A) _
 ∀∈ P xs = ∀ {x} → x ∈ xs → P x
 
+∀∈-syntax : ∀ {p} (P : Pred A p) → Pred (List A) _
+∀∈-syntax = ∀∈
+
+syntax ∀∈-syntax (λ x → P) xs = ∀[ x ∈ xs ] P
+
 ------------------------------------------------------------------------
 -- Operations
 
@@ -45,7 +55,7 @@ _∷=_ = Any._∷=_ {A = A}
 _─_ = Any._─_ {A = A}
 
 mapWith∈ : ∀ {b} {B : Set b}
-           (xs : List A) → (∀∈ (const B) xs) → List B
+           (xs : List A) → ∀[ _ ∈ xs ] B → List B
 mapWith∈ []       f = []
 mapWith∈ (x ∷ xs) f = f (here refl) ∷ mapWith∈ xs (f ∘ there)
 
@@ -54,7 +64,7 @@ mapWith∈ (x ∷ xs) f = f (here refl) ∷ mapWith∈ xs (f ∘ there)
 
 module _ {p} {P : Pred A p} where
 
-  find : ∀ {xs} → Any P xs → ∃∈ P xs
+  find : ∀ {xs} → Any P xs → ∃[ x ∈ xs ] P x
   find (here px)   = _ , here refl , px
   find (there pxs) = let x , x∈xs , px = find pxs in x , there x∈xs , px
 

From c83f5f87c379d13aea9c6b688009f627af577f57 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 6 Apr 2024 21:05:29 +0100
Subject: [PATCH 40/47] =?UTF-8?q?remove`=E2=8A=A5-elim`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

diff --git a/src/Data/List/Relation/Unary/All/Properties.agda b/src/Data/List/Relation/Unary/All/Properties.agda
index 209201d825..9e3c4968c8 100644
--- a/src/Data/List/Relation/Unary/All/Properties.agda
+++ b/src/Data/List/Relation/Unary/All/Properties.agda
@@ -11,7 +11,6 @@ module Data.List.Relation.Unary.All.Properties where
 open import Axiom.Extensionality.Propositional using (Extensionality)
 open import Data.Bool.Base using (Bool; T; true; false)
 open import Data.Bool.Properties using (T-∧)
-open import Data.Empty using (⊥-elim)
 open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.List.Base as List hiding (lookup; updateAt)
 open import Data.List.Membership.Propositional using (_∈_; _≢∈_)
@@ -98,7 +97,7 @@ All¬⇒¬Any (¬p ∷ _)  (here  p) = ¬p p
 All¬⇒¬Any (_  ∷ ¬p) (there p) = All¬⇒¬Any ¬p p
 
 ¬All⇒Any¬ : Decidable P → ∀ xs → ¬ All P xs → Any (¬_ ∘ P) xs
-¬All⇒Any¬ dec []       ¬∀ = ⊥-elim (¬∀ [])
+¬All⇒Any¬ dec []       ¬∀ = contradiction [] ¬∀
 ¬All⇒Any¬ dec (x ∷ xs) ¬∀ with dec x
 ... |  true because  [p] = there (¬All⇒Any¬ dec xs (¬∀ ∘ _∷_ (invert [p])))
 ... | false because [¬p] = here (invert [¬p])
@@ -133,7 +132,7 @@ private
   -- equivalence could be strengthened to a surjection.
   to∘from : Extensionality _ _ → (dec : Decidable P) →
             (¬∀ : ¬ All P xs) → Any¬⇒¬All (¬All⇒Any¬ dec xs ¬∀) ≡ ¬∀
-  to∘from ext P ¬∀ = ext (⊥-elim ∘ ¬∀)
+  to∘from ext P ¬∀ = ext λ ∀P → contradiction ∀P ¬∀
 
 module _ {_~_ : REL A B ℓ} where
 
@@ -218,7 +217,7 @@ updateAt-minimal : ∀ (i : x ∈ xs) (j : y ∈ xs) →
                    pxs              [ i ]= px →
                    updateAt j f pxs [ i ]= px
 updateAt-minimal (here .refl) (here refl) (px ∷ pxs) i≢j here        =
-  ⊥-elim (i≢j refl refl)
+  contradiction refl (i≢j refl)
 updateAt-minimal (here .refl) (there j)   (px ∷ pxs) i≢j here        = here
 updateAt-minimal (there i)    (here refl) (px ∷ pxs) i≢j (there val) = there val
 updateAt-minimal (there i)    (there j)   (px ∷ pxs) i≢j (there val) =
@@ -311,7 +310,7 @@ updateAt-commutes : ∀ (i : x ∈ xs) (j : y ∈ xs) →
                     i ≢∈ j →
                     updateAt {P = P} i f ∘ updateAt j g ≗ updateAt j g ∘ updateAt i f
 updateAt-commutes (here refl) (here refl) i≢j (px ∷ pxs) =
-  ⊥-elim (i≢j refl refl)
+  contradiction refl (i≢j refl)
 updateAt-commutes (here refl) (there j)   i≢j (px ∷ pxs) = refl
 updateAt-commutes (there i)   (here refl) i≢j (px ∷ pxs) = refl
 updateAt-commutes (there i)   (there j)   i≢j (px ∷ pxs) =

From 1f5397e1214cea4e26c0ceb29d18615db5bcb5bc Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 6 Apr 2024 21:06:59 +0100
Subject: [PATCH 41/47] reordered `CHANGELOG`

---
 CHANGELOG.md | 30 +++++++++++++++---------------
 1 file changed, 15 insertions(+), 15 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index e522564482..2a2854b7d4 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -305,6 +305,21 @@ Additions to existing modules
   reverse-downFrom      : reverse (downFrom n) ≡ upTo n
   ```
 
+* In `Data.List.Relation.Binary.Pointwise.Base`:
+  ```agda
+  unzip : Pointwise (R ; S) ⇒ (Pointwise R ; Pointwise S)
+  ```
+
+* In `Data.Maybe.Relation.Binary.Pointwise`:
+  ```agda
+  pointwise⊆any : Pointwise R (just x) ⊆ Any (R x)
+  ```
+
+* In `Data.List.Relation.Binary.Sublist.Setoid`:
+  ```agda
+  ⊆-upper-bound : ∀ {xs ys zs} (τ : xs ⊆ zs) (σ : ys ⊆ zs) → UpperBound τ σ
+  ```
+
 * In `Data.List.Relation.Unary.All`:
   ```agda
   universal-U : Universal (All U)
@@ -354,21 +369,6 @@ Additions to existing modules
                          ∃[ xs ] Appending Y U as bs xs × Appending V R xs cs ds
   ```
 
-* In `Data.List.Relation.Binary.Pointwise.Base`:
-  ```agda
-  unzip : Pointwise (R ; S) ⇒ (Pointwise R ; Pointwise S)
-  ```
-
-* In `Data.Maybe.Relation.Binary.Pointwise`:
-  ```agda
-  pointwise⊆any : Pointwise R (just x) ⊆ Any (R x)
-  ```
-
-* In `Data.List.Relation.Binary.Sublist.Setoid`:
-  ```agda
-  ⊆-upper-bound : ∀ {xs ys zs} (τ : xs ⊆ zs) (σ : ys ⊆ zs) → UpperBound τ σ
-  ```
-
 * In `Data.Nat.Divisibility`:
   ```agda
   quotient≢0       : m ∣ n → .{{NonZero n}} → NonZero quotient

From e3d2665364ffeb94d081c8a6e2f246ddbf7e1147 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 6 Apr 2024 21:21:04 +0100
Subject: [PATCH 42/47] revise combinator names

---
 CHANGELOG.md                                         | 12 +++++++-----
 .../Membership/Propositional/Properties/Core.agda    |  6 +++---
 src/Data/List/Membership/Setoid.agda                 | 12 ++++++------
 src/Data/List/Relation/Unary/All.agda                | 10 +++++-----
 4 files changed, 21 insertions(+), 19 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2a2854b7d4..35cc33e79d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -278,17 +278,19 @@ Additions to existing modules
 
 * In `Data.List.Membership.Propositional.Properties.Core`:
   ```agda
-  find∘∃∈-Any : (p : ∃∈ P xs) → find (∃∈-Any p) ≡ p
+  find∘∃∈-Any : (p : ∃[x∈xs] P xs) → find (∃∈-Any p) ≡ p
   ∃∈-Any∘find : (p : Any P xs) → ∃∈-Any (find p) ≡ p
   ```
 
 * In `Data.List.Membership.Setoid`: two abbreviations for predicate transformers,
   with associated `syntax` declarations
   ```agda
-  ∃∈-syntax : ∀ {p} (P : Pred A p) → Pred (List A) _
-  ∃∈-syntax P xs = ∃ λ x → x ∈ xs × P x
-  ∀∈-syntax : ∀ {p} (P : Pred A p) → Pred (List A) _
-  ∀∈-syntax P xs = ∀ {x} → x ∈ xs → P x
+  ∃[x∈xs] : ∀ {p} (P : Pred A p) → Pred (List A) _
+  ∃[x∈xs] P xs = ∃ λ x → x ∈ xs × P x
+  ∃∈-syntax = ∃[x∈xs]
+  ∀[x∈xs] : ∀ {p} (P : Pred A p) → Pred (List A) _
+  ∀[x∈xs] P xs = ∀ {x} → x ∈ xs → P x
+  ∀∈-syntax = ∀[x∈xs]
   syntax ∃∈-syntax (λ x → P) xs = ∃[ x ∈ xs ] P
   syntax ∀∈-syntax (λ x → P) xs = ∀[ x ∈ xs ] P
   ```
diff --git a/src/Data/List/Membership/Propositional/Properties/Core.agda b/src/Data/List/Membership/Propositional/Properties/Core.agda
index 25693e8a81..2e31d44d4c 100644
--- a/src/Data/List/Membership/Propositional/Properties/Core.agda
+++ b/src/Data/List/Membership/Propositional/Properties/Core.agda
@@ -60,17 +60,17 @@ module _ {P : Pred A p} where
 
 module _ {P : Pred A p} where
 
-  ∃∈-Any : ∃∈ P xs → Any P xs
+  ∃∈-Any : ∃[x∈xs] P xs → Any P xs
   ∃∈-Any (x , x∈xs , px) = lose {P = P} x∈xs px
 
   ∃∈-Any∘find : (p : Any P xs) → ∃∈-Any (find p) ≡ p
   ∃∈-Any∘find p = map∘find p refl
 
-  find∘∃∈-Any : (p : ∃∈ P xs) → find (∃∈-Any p) ≡ p
+  find∘∃∈-Any : (p : ∃[x∈xs] P xs) → find (∃∈-Any p) ≡ p
   find∘∃∈-Any p@(x , x∈xs , px)
     rewrite find∘map x∈xs (flip (resp P) px) | find-∈ x∈xs = refl
 
-  Any↔ : ∃∈ P xs ↔ Any P xs
+  Any↔ : ∃[x∈xs] P xs ↔ Any P xs
   Any↔ = mk↔ₛ′ ∃∈-Any find ∃∈-Any∘find find∘∃∈-Any
 
 ------------------------------------------------------------------------
diff --git a/src/Data/List/Membership/Setoid.agda b/src/Data/List/Membership/Setoid.agda
index 500d55a9c9..9736ecb689 100644
--- a/src/Data/List/Membership/Setoid.agda
+++ b/src/Data/List/Membership/Setoid.agda
@@ -32,19 +32,19 @@ x ∈ xs = Any (x ≈_) xs
 _∉_ : A → List A → Set _
 x ∉ xs = ¬ x ∈ xs
 
-∃∈ : ∀ {p} (P : Pred A p) → Pred (List A) _
-∃∈ P xs = ∃ λ x → x ∈ xs × P x
+∃[x∈xs] : ∀ {p} (P : Pred A p) → Pred (List A) _
+∃[x∈xs] P xs = ∃ λ x → x ∈ xs × P x
 
 ∃∈-syntax : ∀ {p} (P : Pred A p) → Pred (List A) _
-∃∈-syntax = ∃∈
+∃∈-syntax = ∃[x∈xs]
 
 syntax ∃∈-syntax (λ x → P) xs = ∃[ x ∈ xs ] P
 
-∀∈ : ∀ {p} (P : Pred A p) → Pred (List A) _
-∀∈ P xs = ∀ {x} → x ∈ xs → P x
+∀[x∈xs] : ∀ {p} (P : Pred A p) → Pred (List A) _
+∀[x∈xs] P xs = ∀ {x} → x ∈ xs → P x
 
 ∀∈-syntax : ∀ {p} (P : Pred A p) → Pred (List A) _
-∀∈-syntax = ∀∈
+∀∈-syntax = ∀[x∈xs]
 
 syntax ∀∈-syntax (λ x → P) xs = ∀[ x ∈ xs ] P
 
diff --git a/src/Data/List/Relation/Unary/All.agda b/src/Data/List/Relation/Unary/All.agda
index f70e1dc1f7..fbd8a3ceb4 100644
--- a/src/Data/List/Relation/Unary/All.agda
+++ b/src/Data/List/Relation/Unary/All.agda
@@ -10,7 +10,7 @@ module Data.List.Relation.Unary.All where
 
 open import Data.List.Base as List using (List; []; _∷_)
 open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
-open import Data.List.Membership.Propositional renaming (_∈_ to _∈ₚ_; ∀∈ to ∀∈ₚ)
+open import Data.List.Membership.Propositional renaming (_∈_ to _∈ₚ_; ∀[x∈xs] to ∀[x∈ₚxs])
 import Data.List.Membership.Setoid as SetoidMembership
 open import Data.Product.Base as Product
   using (∃; -,_; _×_; _,_; proj₁; proj₂; uncurry)
@@ -119,11 +119,11 @@ module _(S : Setoid a ℓ) {P : Pred (Setoid.Carrier S) p} where
   open Setoid S renaming (refl to ≈-refl)
   open SetoidMembership S
 
-  tabulateₛ : ∀∈ P xs → All P xs
+  tabulateₛ : ∀[x∈xs] P ⊆ All P
   tabulateₛ {[]}    hyp = []
   tabulateₛ {_ ∷ _} hyp = hyp (here ≈-refl) ∷ tabulateₛ (hyp ∘ there)
 
-tabulate : ∀∈ₚ P xs → All P xs
+tabulate : ∀[x∈ₚxs] P ⊆ All P
 tabulate = tabulateₛ (≡.setoid _)
 
 self : ∀ {xs} → All (const A) xs
@@ -191,14 +191,14 @@ lookupAny (px ∷ pxs) (there i) = lookupAny pxs i
 lookupWith : ∀[ P ⇒ Q ⇒ R ] → All P xs → (i : Any Q xs) → R (Any.lookup i)
 lookupWith f pxs i = Product.uncurry f (lookupAny pxs i)
 
-lookup : All P xs → ∀∈ₚ P xs
+lookup : All P ⊆ ∀[x∈ₚxs] P
 lookup pxs = lookupWith (λ { px refl → px }) pxs
 
 module _(S : Setoid a ℓ) {P : Pred (Setoid.Carrier S) p} where
   open Setoid S renaming (sym to ≈-sym)
   open SetoidMembership S
 
-  lookupₛ : P Respects _≈_ → All P xs → ∀∈ P xs
+  lookupₛ : P Respects _≈_ → All P ⊆ ∀[x∈xs] P
   lookupₛ resp pxs = lookupWith (λ py x≈y → resp (≈-sym x≈y) py) pxs
 
 ------------------------------------------------------------------------

From bb3a131e99fae00de7bb818f9f83c1ebcafef49a Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Mon, 8 Apr 2024 08:23:54 +0100
Subject: [PATCH 43/47] tighten `import`s

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

diff --git a/src/Data/List/Relation/Unary/Any/Properties.agda b/src/Data/List/Relation/Unary/Any/Properties.agda
index 7b521de31f..24eb66852b 100644
--- a/src/Data/List/Relation/Unary/Any/Properties.agda
+++ b/src/Data/List/Relation/Unary/Any/Properties.agda
@@ -45,9 +45,10 @@ open import Relation.Binary.PropositionalEquality.Properties
   using (module ≡-Reasoning)
 open import Relation.Unary as U
   using (Pred; _⟨×⟩_; _⟨→⟩_) renaming (_⊆_ to _⋐_)
-open import Relation.Nullary using (¬_; _because_; does; invert; yes; no)
-open import Relation.Nullary.Decidable using (¬?; decidable-stable)
-open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Nullary.Decidable.Core
+  using (¬?; _because_; does; yes; no; decidable-stable)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
+open import Relation.Nullary.Reflects using (invert)
 
 private
   open module ListMonad {ℓ} = RawMonad (monad {ℓ = ℓ})

From c5b3341f75d4ff3b1d09c0c02d0f993363c7c4ab Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Mon, 8 Apr 2024 08:46:04 +0100
Subject: [PATCH 44/47] tighten `import`s

---
 src/Data/List/Membership/Propositional/Properties.agda | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/Data/List/Membership/Propositional/Properties.agda b/src/Data/List/Membership/Propositional/Properties.agda
index d6e343b948..9a2f927aff 100644
--- a/src/Data/List/Membership/Propositional/Properties.agda
+++ b/src/Data/List/Membership/Propositional/Properties.agda
@@ -39,8 +39,9 @@ open import Relation.Binary.Definitions as Binary hiding (Decidable)
 open import Relation.Binary.PropositionalEquality as ≡
   using (_≡_; _≢_; refl; sym; trans; cong; resp; _≗_)
 import Relation.Binary.Properties.DecTotalOrder as DTOProperties
-open import Relation.Nullary.Decidable using (Dec; yes; no; ¬¬-excluded-middle)
-open import Relation.Nullary.Negation using (¬_; contradiction)
+open import Relation.Nullary.Decidable.Core
+  using (Dec; yes; no; ¬¬-excluded-middle)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Unary using (_⟨×⟩_; Decidable)
 

From 93eaaa5c34a636dcc08ed7e61847e4f0455ec9ec Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 22 Apr 2024 06:34:19 +0100
Subject: [PATCH 45/47] fixed merge conflict bug

---
 src/Data/List/Membership/Propositional/Properties.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/List/Membership/Propositional/Properties.agda b/src/Data/List/Membership/Propositional/Properties.agda
index f539923836..99cecaac17 100644
--- a/src/Data/List/Membership/Propositional/Properties.agda
+++ b/src/Data/List/Membership/Propositional/Properties.agda
@@ -40,7 +40,7 @@ open import Level using (Level)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Definitions as Binary hiding (Decidable)
 open import Relation.Binary.PropositionalEquality.Core as ≡
-  using (_≡_; _≢_; refl; sym; trans; cong; resp; _≗_)
+  using (_≡_; _≢_; refl; sym; trans; cong; cong₂; resp; _≗_)
 open import Relation.Binary.PropositionalEquality.Properties as ≡ using (setoid)
 import Relation.Binary.Properties.DecTotalOrder as DTOProperties
 open import Relation.Nullary.Decidable.Core

From 70c0f16606c72e4a8ee850948fde7844c3520c92 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 22 Apr 2024 07:14:15 +0100
Subject: [PATCH 46/47] removed new syntax

---
 CHANGELOG.md                                  | 15 +-------------
 .../Propositional/Properties/Core.agda        |  8 ++++----
 src/Data/List/Membership/Setoid.agda          | 20 ++-----------------
 3 files changed, 7 insertions(+), 36 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index d4af482bdc..918ff6a7c8 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -329,23 +329,10 @@ Additions to existing modules
 
 * In `Data.List.Membership.Propositional.Properties.Core`:
   ```agda
-  find∘∃∈-Any : (p : ∃[x∈xs] P xs) → find (∃∈-Any p) ≡ p
+  find∘∃∈-Any : (p : ∃ λ x → x ∈ xs × P x) → find (∃∈-Any p) ≡ p
   ∃∈-Any∘find : (p : Any P xs) → ∃∈-Any (find p) ≡ p
   ```
 
-* In `Data.List.Membership.Setoid`: two abbreviations for predicate transformers,
-  with associated `syntax` declarations
-  ```agda
-  ∃[x∈xs] : ∀ {p} (P : Pred A p) → Pred (List A) _
-  ∃[x∈xs] P xs = ∃ λ x → x ∈ xs × P x
-  ∃∈-syntax = ∃[x∈xs]
-  ∀[x∈xs] : ∀ {p} (P : Pred A p) → Pred (List A) _
-  ∀[x∈xs] P xs = ∀ {x} → x ∈ xs → P x
-  ∀∈-syntax = ∀[x∈xs]
-  syntax ∃∈-syntax (λ x → P) xs = ∃[ x ∈ xs ] P
-  syntax ∀∈-syntax (λ x → P) xs = ∀[ x ∈ xs ] P
-  ```
-
 * In `Data.List.Properties`:
   ```agda
   length-catMaybes      : length (catMaybes xs) ≤ length xs
diff --git a/src/Data/List/Membership/Propositional/Properties/Core.agda b/src/Data/List/Membership/Propositional/Properties/Core.agda
index 2e31d44d4c..5c77e40b96 100644
--- a/src/Data/List/Membership/Propositional/Properties/Core.agda
+++ b/src/Data/List/Membership/Propositional/Properties/Core.agda
@@ -15,7 +15,7 @@ module Data.List.Membership.Propositional.Properties.Core where
 open import Data.List.Base using (List)
 open import Data.List.Membership.Propositional
 open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
-open import Data.Product.Base as Product using (_,_)
+open import Data.Product.Base as Product using (_,_; ∃; _×_)
 open import Function.Base using (flip; id; _∘_)
 open import Function.Bundles using (_↔_; mk↔ₛ′)
 open import Level using (Level)
@@ -60,17 +60,17 @@ module _ {P : Pred A p} where
 
 module _ {P : Pred A p} where
 
-  ∃∈-Any : ∃[x∈xs] P xs → Any P xs
+  ∃∈-Any : (∃ λ x → x ∈ xs × P x) → Any P xs
   ∃∈-Any (x , x∈xs , px) = lose {P = P} x∈xs px
 
   ∃∈-Any∘find : (p : Any P xs) → ∃∈-Any (find p) ≡ p
   ∃∈-Any∘find p = map∘find p refl
 
-  find∘∃∈-Any : (p : ∃[x∈xs] P xs) → find (∃∈-Any p) ≡ p
+  find∘∃∈-Any : (p : ∃ λ x → x ∈ xs × P x) → find (∃∈-Any p) ≡ p
   find∘∃∈-Any p@(x , x∈xs , px)
     rewrite find∘map x∈xs (flip (resp P) px) | find-∈ x∈xs = refl
 
-  Any↔ : ∃[x∈xs] P xs ↔ Any P xs
+  Any↔ : (∃ λ x → x ∈ xs × P x) ↔ Any P xs
   Any↔ = mk↔ₛ′ ∃∈-Any find ∃∈-Any∘find find∘∃∈-Any
 
 ------------------------------------------------------------------------
diff --git a/src/Data/List/Membership/Setoid.agda b/src/Data/List/Membership/Setoid.agda
index 9736ecb689..b1ff4f2773 100644
--- a/src/Data/List/Membership/Setoid.agda
+++ b/src/Data/List/Membership/Setoid.agda
@@ -32,22 +32,6 @@ x ∈ xs = Any (x ≈_) xs
 _∉_ : A → List A → Set _
 x ∉ xs = ¬ x ∈ xs
 
-∃[x∈xs] : ∀ {p} (P : Pred A p) → Pred (List A) _
-∃[x∈xs] P xs = ∃ λ x → x ∈ xs × P x
-
-∃∈-syntax : ∀ {p} (P : Pred A p) → Pred (List A) _
-∃∈-syntax = ∃[x∈xs]
-
-syntax ∃∈-syntax (λ x → P) xs = ∃[ x ∈ xs ] P
-
-∀[x∈xs] : ∀ {p} (P : Pred A p) → Pred (List A) _
-∀[x∈xs] P xs = ∀ {x} → x ∈ xs → P x
-
-∀∈-syntax : ∀ {p} (P : Pred A p) → Pred (List A) _
-∀∈-syntax = ∀[x∈xs]
-
-syntax ∀∈-syntax (λ x → P) xs = ∀[ x ∈ xs ] P
-
 ------------------------------------------------------------------------
 -- Operations
 
@@ -55,7 +39,7 @@ _∷=_ = Any._∷=_ {A = A}
 _─_ = Any._─_ {A = A}
 
 mapWith∈ : ∀ {b} {B : Set b}
-           (xs : List A) → ∀[ _ ∈ xs ] B → List B
+           (xs : List A) → (∀ {x} → x ∈ xs → B) → List B
 mapWith∈ []       f = []
 mapWith∈ (x ∷ xs) f = f (here refl) ∷ mapWith∈ xs (f ∘ there)
 
@@ -64,7 +48,7 @@ mapWith∈ (x ∷ xs) f = f (here refl) ∷ mapWith∈ xs (f ∘ there)
 
 module _ {p} {P : Pred A p} where
 
-  find : ∀ {xs} → Any P xs → ∃[ x ∈ xs ] P x
+  find : ∀ {xs} → Any P xs → ∃ λ x → x ∈ xs × P x
   find (here px)   = _ , here refl , px
   find (there pxs) = let x , x∈xs , px = find pxs in x , there x∈xs , px
 

From 9ec7a37bc7151079956f102d96f0062c09b71ced Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 22 Apr 2024 07:19:04 +0100
Subject: [PATCH 47/47] knock-on

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

diff --git a/src/Data/List/Relation/Unary/All.agda b/src/Data/List/Relation/Unary/All.agda
index fbd8a3ceb4..ea2ab858df 100644
--- a/src/Data/List/Relation/Unary/All.agda
+++ b/src/Data/List/Relation/Unary/All.agda
@@ -10,7 +10,7 @@ module Data.List.Relation.Unary.All where
 
 open import Data.List.Base as List using (List; []; _∷_)
 open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
-open import Data.List.Membership.Propositional renaming (_∈_ to _∈ₚ_; ∀[x∈xs] to ∀[x∈ₚxs])
+open import Data.List.Membership.Propositional renaming (_∈_ to _∈ₚ_)
 import Data.List.Membership.Setoid as SetoidMembership
 open import Data.Product.Base as Product
   using (∃; -,_; _×_; _,_; proj₁; proj₂; uncurry)
@@ -119,11 +119,11 @@ module _(S : Setoid a ℓ) {P : Pred (Setoid.Carrier S) p} where
   open Setoid S renaming (refl to ≈-refl)
   open SetoidMembership S
 
-  tabulateₛ : ∀[x∈xs] P ⊆ All P
+  tabulateₛ : (∀ {x} → x ∈ xs → P x) → All P xs
   tabulateₛ {[]}    hyp = []
   tabulateₛ {_ ∷ _} hyp = hyp (here ≈-refl) ∷ tabulateₛ (hyp ∘ there)
 
-tabulate : ∀[x∈ₚxs] P ⊆ All P
+tabulate : (∀ {x} → x ∈ₚ xs → P x) → All P xs
 tabulate = tabulateₛ (≡.setoid _)
 
 self : ∀ {xs} → All (const A) xs
@@ -191,14 +191,14 @@ lookupAny (px ∷ pxs) (there i) = lookupAny pxs i
 lookupWith : ∀[ P ⇒ Q ⇒ R ] → All P xs → (i : Any Q xs) → R (Any.lookup i)
 lookupWith f pxs i = Product.uncurry f (lookupAny pxs i)
 
-lookup : All P ⊆ ∀[x∈ₚxs] P
+lookup : All P xs → (∀ {x} → x ∈ₚ xs → P x)
 lookup pxs = lookupWith (λ { px refl → px }) pxs
 
 module _(S : Setoid a ℓ) {P : Pred (Setoid.Carrier S) p} where
   open Setoid S renaming (sym to ≈-sym)
   open SetoidMembership S
 
-  lookupₛ : P Respects _≈_ → All P ⊆ ∀[x∈xs] P
+  lookupₛ : P Respects _≈_ → All P xs → (∀ {x} → x ∈ xs → P x)
   lookupₛ resp pxs = lookupWith (λ py x≈y → resp (≈-sym x≈y) py) pxs
 
 ------------------------------------------------------------------------