From c0fafe970d46f64ebd755a854c7c91b41fd2993f Mon Sep 17 00:00:00 2001
From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Date: Wed, 5 Jun 2024 16:46:06 +0100
Subject: [PATCH] Refactor `List.Membership.*` and `List.Relation.Unary.Any`
 (#2324)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* `contradiction` against `⊥-elim`

* tightened `import`s

* added two operations `∃∈` and `∀∈`

* added to `CHANGELOG`

* knock-on for the `Propositional` case

* refactor `lose∘find` and `find∘lose` in terms of new lemmas `∃∈-Any∘find` and `find∘∃∈-Any`

* `CHANGELOG`

* reorder

* knock-on viscosity

* knock-on viscosity; plus refactoring of `×↔` for intelligibility

* knock-on viscosity

* tightened `import`s

* misc. import and other tweaks

* misc. import and other tweaks

* misc. import and other tweaks

* removed spurious module name

* better definition of `find`

* make intermediate terms explicit in proof of `to∘from`

* tweaks

* Update Setoid.agda

Remove redundant import of `index` from `Any`

* Update Setoid.agda

Removed more redundant `import`ed operations

* Update Properties.agda

Another redundant `import`

* Update Properties.agda

Another redundant `import`ed operation

* `with` into `let`

* `with` into `let`

* `with` into `let`

* `with` into `let`

* indentation

* fix `universal-U`

* added `map-cong`

* deprecate `map-compose` in favour of `map-∘`

* explicit `let` in statement of `find∘map`

* knock-on viscosity: hide `map-cong`

* use of `Product.map₁`

* revert use of `Product.map₁`

* inlined lemmas!

* alpha conversion and further inlining!

* correctted use of `Product.map₂`

* added `syntax` declarations for the new combinators

* remove`⊥-elim`

* reordered `CHANGELOG`

* revise combinator names

* tighten `import`s

* tighten `import`s

* fixed merge conflict bug

* removed new syntax

* knock-on
---
 CHANGELOG.md                                  |  64 +++++---
 src/Data/List/Membership/Propositional.agda   |   4 +-
 .../Membership/Propositional/Properties.agda  |  79 +++++----
 .../Propositional/Properties/Core.agda        |  87 +++++-----
 src/Data/List/Membership/Setoid.agda          |  14 +-
 .../List/Membership/Setoid/Properties.agda    |  64 ++++----
 .../Relation/Binary/BagAndSetEquality.agda    |  24 +--
 src/Data/List/Relation/Unary/All.agda         |  23 +--
 .../List/Relation/Unary/All/Properties.agda   |  77 +++++----
 src/Data/List/Relation/Unary/Any.agda         |   5 +-
 .../List/Relation/Unary/Any/Properties.agda   | 154 ++++++++++--------
 11 files changed, 319 insertions(+), 276 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index e02ff2dc30..156756ff00 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -82,16 +82,9 @@ Deprecated names
   scanl-defn  ↦  Data.List.Scans.Properties.scanl-defn
   ```
 
-* In `Data.List.NonEmpty.Base`:
-  ```agda
-  inits : List A → List⁺ (List A)
-  tails : List A → List⁺ (List A)
-  ```
-
-* In `Data.List.NonEmpty.Properties`:
+* In `Data.List.Relation.Unary.All.Properties`:
   ```agda
-  toList-inits : toList ∘ List⁺.inits ≗ List.inits
-  toList-tails : toList ∘ List⁺.tails ≗ List.tails
+  map-compose  ↦  map-∘
   ```
 
 * In `Data.Nat.Divisibility.Core`:
@@ -412,6 +405,12 @@ Additions to existing modules
   tail∘tails : List A → List (List A)
   ```
 
+* In `Data.List.Membership.Propositional.Properties.Core`:
+  ```agda
+  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.Properties`:
   ```agda
   reverse⁺ : x ∈ xs → x ∈ reverse xs
@@ -424,6 +423,12 @@ Additions to existing modules
   tails : List A → List⁺ (List A)
   ```
 
+* In `Data.List.NonEmpty.Properties`:
+  ```agda
+  toList-inits : toList ∘ List⁺.inits ≗ List.inits
+  toList-tails : toList ∘ List⁺.tails ≗ List.tails
+  ```
+
 * In `Data.List.Properties`:
   ```agda
   length-catMaybes       : length (catMaybes xs) ≤ length xs
@@ -477,6 +482,21 @@ Additions to existing modules
   mapMaybeIsInj₂∘mapInj₁ : mapMaybe isInj₂ (map inj₁ xs) ≡ []
   ```
 
+* 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.Binary.Sublist.Setoid.Properties`:
   ```agda
   ⊆-trans-idˡ   : (trans-reflˡ : ∀ {x y} (p : x ≈ y) → trans ≈-refl p ≡ p) →
@@ -498,6 +518,11 @@ Additions to existing modules
   reverse⁻            : reverse as ⊆ reverse bs → as ⊆ bs
   ```
 
+* 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)
@@ -510,6 +535,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 →
@@ -536,21 +567,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
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 _)
diff --git a/src/Data/List/Membership/Propositional/Properties.agda b/src/Data/List/Membership/Propositional/Properties.agda
index f93bf81f4a..03e31d8aae 100644
--- a/src/Data/List/Membership/Propositional/Properties.agda
+++ b/src/Data/List/Membership/Propositional/Properties.agda
@@ -10,26 +10,26 @@ module Data.List.Membership.Propositional.Properties where
 
 open import Algebra.Core using (Op₂)
 open import Algebra.Definitions using (Selective)
-open import Effect.Monad using (RawMonad)
-open import Data.Bool.Base using (Bool; false; true; T)
 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
-  using (map↔; concat↔; >>=↔; ⊛↔; Any-cong; ⊗↔′; ¬Any[])
+open import Data.List.Effectful using (monad)
 open import Data.List.Membership.Propositional
   using (_∈_; _∉_; mapWith∈; _≢∈_)
 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.Nat.Properties using (_≤?_; m≤n⇒m≤1+n; ≤ᵇ-reflects-≤; <⇒≢; ≰⇒>)
+open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
+open import Data.List.Relation.Unary.Any.Properties
+  using (map↔; concat↔; >>=↔; ⊛↔; Any-cong; ⊗↔′; ¬Any[])
+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 using (∃; ∃₂; _×_; _,_)
 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 using (_∘_; _∘′_; _$_; id; flip; _⟨_⟩_)
 open import Function.Definitions using (Injective)
 import Function.Related.Propositional as Related
@@ -40,15 +40,14 @@ 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; cong₂; subst; _≗_)
+  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.Unary using (_⟨×⟩_; Decidable)
-import Relation.Nullary.Reflects as Reflects
+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.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 {ℓ = ℓ})
@@ -128,8 +127,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
@@ -147,8 +147,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 =
+    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
@@ -183,8 +184,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
@@ -205,8 +207,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
@@ -227,8 +228,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
@@ -247,10 +247,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
@@ -310,7 +310,7 @@ module _ (_≈?_ : DecidableEquality 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 _)
 
 ------------------------------------------------------------------------
@@ -365,28 +365,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 ca8ffbb1ea..5c77e40b96 100644
--- a/src/Data/List/Membership/Propositional/Properties/Core.agda
+++ b/src/Data/List/Membership/Propositional/Properties/Core.agda
@@ -12,75 +12,74 @@
 
 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.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↔ₛ′)
 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.
 
-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
+module _ {P : Pred A p} where
 
-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
+  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∘map : ∀ {Q : Pred A q} {xs} (p : Any P xs) (f : P ⊆ Q) →
+             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
 
 ------------------------------------------------------------------------
 -- 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 : (∃ λ 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 → 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↔ : ∀ {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))
+  Any↔ : (∃ λ x → x ∈ xs × P x) ↔ Any P xs
+  Any↔ = mk↔ₛ′ ∃∈-Any find ∃∈-Any∘find find∘∃∈-Any
+
+------------------------------------------------------------------------
+-- 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)
diff --git a/src/Data/List/Membership/Setoid.agda b/src/Data/List/Membership/Setoid.agda
index cadc600646..b1ff4f2773 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)
-open import Data.List.Base as List using (List; []; _∷_; length; lookup)
+open import Data.List.Base using (List; []; _∷_)
 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 Relation.Unary using (Pred)
+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)
 
 open Setoid S renaming (Carrier to A)
 
@@ -49,8 +49,8 @@ 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 (there pxs) = Product.map id (Product.map there id) (find pxs)
+  find (here px)   = _ , here refl , 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
diff --git a/src/Data/List/Membership/Setoid/Properties.agda b/src/Data/List/Membership/Setoid/Properties.agda
index a0fcb4881b..48303dec37 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,10 @@ 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) =
+    let hs , _ , _ , v≈v′ , eq = ∈-∃++ v∈xs
+    in d ∷ hs , _ , _ , v≈v′ , refl ∷ eq
 
 ------------------------------------------------------------------------
 -- concat
@@ -235,8 +235,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] =
+    let xs , xs∈xss , v∈xs = find (∈-concat⁻ xss v∈c[xss]) in xs , v∈xs , xs∈xss
 
 ------------------------------------------------------------------------
 -- reverse
@@ -271,10 +271,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
@@ -388,9 +390,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
diff --git a/src/Data/List/Relation/Binary/BagAndSetEquality.agda b/src/Data/List/Relation/Binary/BagAndSetEquality.agda
index 9c400fdcff..815b27db89 100644
--- a/src/Data/List/Relation/Binary/BagAndSetEquality.agda
+++ b/src/Data/List/Relation/Binary/BagAndSetEquality.agda
@@ -30,7 +30,7 @@ open import Data.List.Relation.Binary.Permutation.Propositional
   using (_↭_; ↭-sym; refl; module PermutationReasoning)
 open import Data.List.Relation.Binary.Permutation.Propositional.Properties
   using (∈-resp-↭; ∈-resp-[σ⁻¹∘σ]; ↭-sym-involutive; shift; ++-comm)
-open import Data.Product.Base as Prod using (∃; _,_; proj₁; proj₂; _×_)
+open import Data.Product.Base as Product using (∃; _,_; proj₁; proj₂; _×_)
 import Data.Product.Function.Dependent.Propositional as Σ
 open import Data.Sum.Base as Sum using (_⊎_; [_,_]′; inj₁; inj₂)
 open import Data.Sum.Properties using (inj₂-injective; inj₁-injective)
@@ -396,13 +396,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₂ (Prod.map id (to xs≈ys)
-      (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)))))   ≡⟨⟩
 
-    to (Fin-length ys) (Prod.map id (to xs≈ys)
-      (from (Fin-length xs) (index-of p)))                          ≡⟨⟩
+    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)                        ∎
+    to (Fin-length-cong xs≈ys) (index-of p)                   ∎
     where
     open ≡-Reasoning
     open Inverse
@@ -429,10 +429,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
 
@@ -520,13 +520,13 @@ drop-cons {x = x} {xs} {ys} x∷xs≈x∷ys =
       g∘g′ | inj₁ a , eq₁ | inj₂ c  , eq₂ | inj₁ a′ , eq₃ | inj₁ a″ , eq₄ = ⊥-elim $ from-hyp eq₃ eq₄
       g∘g′ | inj₁ a , eq₁ | inj₂ c  , eq₂ | inj₁ a′ , eq₃ | inj₂ b′ , eq₄ = inj₂-injective (
         let lemma =
-              inj₁ a′             ≡⟨ ≡.sym eq₃ ⟩
+              inj₁ a′            ≡⟨ ≡.sym eq₃ ⟩
               from f (inj₂ c)    ≡⟨ to-from f eq₂ ⟩
               inj₁ a             ∎
         in
         inj₂ b′             ≡⟨ ≡.sym eq₄ ⟩
         from f (inj₁ a′)    ≡⟨ ≡.cong (from f ∘ inj₁) $ inj₁-injective lemma ⟩
-        from f (inj₁ a)    ≡⟨ to-from f eq₁ ⟩
+        from f (inj₁ a)     ≡⟨ to-from f eq₁ ⟩
         inj₂ b              ∎)
 
   -- Some final lemmas.
diff --git a/src/Data/List/Relation/Unary/All.agda b/src/Data/List/Relation/Unary/All.agda
index bd8677630b..ea2ab858df 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 _∈ₚ_)
@@ -18,11 +15,14 @@ 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)
 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 +68,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 +116,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ₛ {[]}    hyp = []
+  tabulateₛ {_ ∷ _} hyp = hyp (here ≈-refl) ∷ tabulateₛ (hyp ∘ there)
 
 tabulate : (∀ {x} → x ∈ₚ xs → P x) → All P xs
 tabulate = tabulateₛ (≡.setoid _)
 
-self : ∀ {xs : List A} → All (const A) xs
+self : ∀ {xs} → All (const A) xs
 self = tabulate (λ {x} _ → x)
 
 ------------------------------------------------------------------------
@@ -195,11 +195,11 @@ 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 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ₛ resp pxs = lookupWith (λ py x≈y → resp (≈-sym x≈y) py) pxs
 
 ------------------------------------------------------------------------
 -- Properties of predicates preserved by All
@@ -212,6 +212,9 @@ universal : Universal P → Universal (All P)
 universal u []       = []
 universal u (x ∷ xs) = u x ∷ universal u xs
 
+universal-U : Universal (All {A = A} U)
+universal-U = universal Unary.U-Universal
+
 irrelevant : Irrelevant P → Irrelevant (All P)
 irrelevant irr []           []           = ≡.refl
 irrelevant irr (px₁ ∷ pxs₁) (px₂ ∷ pxs₂) =
diff --git a/src/Data/List/Relation/Unary/All/Properties.agda b/src/Data/List/Relation/Unary/All/Properties.agda
index c77df039d2..9e3c4968c8 100644
--- a/src/Data/List/Relation/Unary/All/Properties.agda
+++ b/src/Data/List/Relation/Unary/All/Properties.agda
@@ -11,23 +11,22 @@ 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.Properties as Listₚ using (partition-defn)
 open import Data.List.Membership.Propositional using (_∈_; _≢∈_)
 open import Data.List.Membership.Propositional.Properties
   using (there-injective-≢∈; ∈-filter⁻)
 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)
@@ -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
 
@@ -177,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)
@@ -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) =
@@ -387,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
@@ -524,7 +522,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)
@@ -596,7 +594,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)
@@ -606,12 +604,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
@@ -620,7 +618,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
 
 ------------------------------------------------------------------------
@@ -636,7 +634,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
@@ -646,8 +644,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
@@ -720,9 +718,10 @@ 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 =
+    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⁻ []         = _
@@ -744,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≈ []            []         = []
@@ -795,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."
+#-}
diff --git a/src/Data/List/Relation/Unary/Any.agda b/src/Data/List/Relation/Unary/Any.agda
index 1b6093cadc..ad9707cd77 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 (∃; _,_)
@@ -17,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
@@ -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
diff --git a/src/Data/List/Relation/Unary/Any/Properties.agda b/src/Data/List/Relation/Unary/Any/Properties.agda
index c91a784ff7..836e73d4a4 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.Function.NonDependent.Propositional
   using (_×-cong_)
 import Data.Product.Function.Dependent.Propositional as Σ
@@ -40,14 +40,15 @@ 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.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 {ℓ = ℓ})
@@ -96,6 +97,11 @@ Any-cong {P = P} {Q = Q} {xs = xs} {ys} P↔Q xs≈ys =
 ------------------------------------------------------------------------
 -- Any.map
 
+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-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
 map-id f hyp (here  p) = cong here (hyp p)
@@ -122,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 ⊥
@@ -212,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
@@ -222,7 +231,7 @@ Any-×⁻ pq with Product.map₂ (Product.map₂ find) (find pq)
   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))
 
@@ -241,10 +250,10 @@ Any-×⁻ pq with Product.map₂ (Product.map₂ find) (find pq)
          (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
@@ -254,24 +263,32 @@ 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
+        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 (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′
+            ∎
+
+    in  begin
+      Any-×⁺ (Any-×⁻ pq)
+        ≡⟨⟩
+      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
+        ∎
 
 ------------------------------------------------------------------------
 -- Half-applied product commutes with Any.
@@ -360,9 +377,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
@@ -459,10 +476,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
@@ -486,8 +503,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) =
+  let i , i<n , q = applyUpTo⁻ (f ∘ suc) p in suc i , s<s i<n , q
 
 ------------------------------------------------------------------------
 -- applyDownFrom
@@ -495,13 +512,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) =
+  let i , i<n , q = applyDownFrom⁻ f p in i , m<n⇒m<1+n i<n , q
 
 ------------------------------------------------------------------------
 -- tabulate
@@ -521,8 +538,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
@@ -536,14 +553,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
@@ -555,9 +572,10 @@ module _ {R : A → A → Set 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)