Merge tag 'upstream/0.17'

Upstream version 0.17

# gpg: Signature made Fri 23 Nov 2018 05:29:18 PM MST
# gpg:                using RSA key 9B917007AE030E36E4FC248B695B7AE4BF066240
# gpg:                issuer "spwhitton@spwhitton.name"
# gpg: Good signature from "Sean Whitton <spwhitton@spwhitton.name>" [ultimate]
# Primary key fingerprint: 8DC2 487E 51AB DD90 B5C4  753F 0F56 D055 3B6D 411B
#      Subkey fingerprint: 9B91 7007 AE03 0E36 E4FC  248B 695B 7AE4 BF06 6240

7 files changed, 772 insertions, 0 deletions

diff --git a/src/Data/List/Membership/DecPropositional.agda b/src/Data/List/Membership/DecPropositional.agda
new file mode 100644
index 0000000..5b59040
--- /dev/null
+++ b/src/Data/List/Membership/DecPropositional.agda
@@ -0,0 +1,19 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Decidable propositional membership over lists
+------------------------------------------------------------------------
+
+open import Relation.Binary using (Decidable)
+open import Relation.Binary.PropositionalEquality using (_≡_; decSetoid)
+
+module Data.List.Membership.DecPropositional
+  {a} {A : Set a} (_≟_ : Decidable (_≡_ {A = A})) where
+
+------------------------------------------------------------------------
+-- Re-export contents of propositional membership
+
+open import Data.List.Membership.Propositional public
+open import Data.List.Membership.DecSetoid (decSetoid _≟_) public
+  using (_∈?_)
+
diff --git a/src/Data/List/Membership/DecSetoid.agda b/src/Data/List/Membership/DecSetoid.agda
new file mode 100644
index 0000000..8ea8548
--- /dev/null
+++ b/src/Data/List/Membership/DecSetoid.agda
@@ -0,0 +1,25 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Decidable setoid membership over lists
+------------------------------------------------------------------------
+
+open import Relation.Binary using (Decidable; DecSetoid)
+
+module Data.List.Membership.DecSetoid {a ℓ} (DS : DecSetoid a ℓ) where
+
+open import Data.List.Any using (any)
+open DecSetoid DS
+
+------------------------------------------------------------------------
+-- Re-export contents of propositional membership
+
+open import Data.List.Membership.Setoid (DecSetoid.setoid DS) public
+
+------------------------------------------------------------------------
+-- Other operations
+
+infix 4 _∈?_
+
+_∈?_ : Decidable _∈_
+x ∈? xs = any (x ≟_) xs
diff --git a/src/Data/List/Membership/Propositional.agda b/src/Data/List/Membership/Propositional.agda
new file mode 100644
index 0000000..0de5e55
--- /dev/null
+++ b/src/Data/List/Membership/Propositional.agda
@@ -0,0 +1,24 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Data.List.Any.Membership instantiated with propositional equality,
+-- along with some additional definitions.
+------------------------------------------------------------------------
+
+module Data.List.Membership.Propositional {a} {A : Set a} where
+
+open import Data.List.Any using (Any)
+open import Relation.Binary.PropositionalEquality using (setoid; subst)
+
+import Data.List.Membership.Setoid as SetoidMembership
+
+------------------------------------------------------------------------
+-- Re-export contents of setoid membership
+
+open SetoidMembership (setoid A) public hiding (lose)
+
+------------------------------------------------------------------------
+-- Other operations
+
+lose : ∀ {p} {P : A → Set p} {x xs} → x ∈ xs → P x → Any P xs
+lose = SetoidMembership.lose (setoid A) (subst _)
diff --git a/src/Data/List/Membership/Propositional/Properties.agda b/src/Data/List/Membership/Propositional/Properties.agda
new file mode 100644
index 0000000..2422c22
--- /dev/null
+++ b/src/Data/List/Membership/Propositional/Properties.agda
@@ -0,0 +1,332 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties related to propositional list membership
+------------------------------------------------------------------------
+
+-- This module does not  treat the general variant of list membership,
+-- parametrised on a setoid, only the variant where the equality is
+-- fixed to be propositional equality.
+
+module Data.List.Membership.Propositional.Properties where
+
+open import Algebra using (CommutativeSemiring)
+open import Algebra.FunctionProperties using (Op₂; Selective)
+open import Category.Monad using (RawMonad)
+open import Data.Bool.Base using (Bool; false; true; T)
+open import Data.Fin using (Fin)
+open import Data.List as List
+open import Data.List.Any as Any using (Any; here; there)
+open import Data.List.Any.Properties
+open import Data.List.Membership.Propositional
+import Data.List.Membership.Setoid.Properties as Membershipₛ
+open import Data.List.Relation.Equality.Propositional
+  using (_≋_; ≡⇒≋; ≋⇒≡)
+open import Data.List.Categorical using (monad)
+open import Data.Nat using (ℕ; zero; suc; pred; s≤s; _≤_; _<_; _≤?_)
+open import Data.Nat.Properties
+open import Data.Product hiding (map)
+open import Data.Product.Relation.Pointwise.NonDependent using (_×-cong_)
+import Data.Product.Relation.Pointwise.Dependent as Σ
+open import Data.Sum as Sum using (_⊎_; inj₁; inj₂)
+open import Function
+open import Function.Equality using (_⟨$⟩_)
+open import Function.Equivalence using (module Equivalence)
+open import Function.Injection using (Injection; Injective; _↣_)
+open import Function.Inverse as Inv using (_↔_; module Inverse)
+import Function.Related as Related
+open import Function.Related.TypeIsomorphisms
+open import Relation.Binary hiding (Decidable)
+open import Relation.Binary.PropositionalEquality as P
+  using (_≡_; _≢_; refl; sym; trans; cong; subst; →-to-⟶; _≗_)
+import Relation.Binary.Properties.DecTotalOrder as DTOProperties
+open import Relation.Unary using (_⟨×⟩_; Decidable)
+open import Relation.Nullary using (¬_; Dec; yes; no)
+open import Relation.Nullary.Negation
+
+private
+  open module ListMonad {ℓ} = RawMonad (monad {ℓ = ℓ})
+
+------------------------------------------------------------------------
+-- Publicly re-export properties from Core
+
+open import Data.List.Membership.Propositional.Properties.Core public
+
+------------------------------------------------------------------------
+-- Equality
+
+module _ {a} {A : Set a} where
+
+  ∈-resp-≋ : ∀ {x} → (x ∈_) Respects _≋_
+  ∈-resp-≋ = Membershipₛ.∈-resp-≋ (P.setoid A)
+
+  ∉-resp-≋ : ∀ {x} → (x ∉_) Respects _≋_
+  ∉-resp-≋ = Membershipₛ.∉-resp-≋ (P.setoid A)
+
+------------------------------------------------------------------------
+-- mapWith∈
+
+module _ {a b} {A : Set a} {B : Set b} where
+
+  mapWith∈-cong : ∀ (xs : List A) → (f g : ∀ {x} → x ∈ xs → B) →
+                  (∀ {x} → (x∈xs : x ∈ xs) → f x∈xs ≡ g x∈xs) →
+                  mapWith∈ xs f ≡ mapWith∈ xs g
+  mapWith∈-cong []       f g cong = refl
+  mapWith∈-cong (x ∷ xs) f g cong = P.cong₂ _∷_ (cong (here refl))
+    (mapWith∈-cong xs (f ∘ there) (g ∘ there) (cong ∘ there))
+
+  mapWith∈≗map : ∀ f xs → mapWith∈ xs (λ {x} _ → f x) ≡ map f xs
+  mapWith∈≗map f xs =
+    ≋⇒≡ (Membershipₛ.mapWith∈≗map (P.setoid A) (P.setoid B) f xs)
+
+------------------------------------------------------------------------
+-- map
+
+module _ {a b} {A : Set a} {B : Set b} {f : A → B} where
+
+  ∈-map⁺ : ∀ {x xs} → x ∈ xs → f x ∈ map f xs
+  ∈-map⁺ = Membershipₛ.∈-map⁺ (P.setoid A) (P.setoid B) (P.cong f)
+
+  ∈-map⁻ : ∀ {y xs} → y ∈ map f xs → ∃ λ x → x ∈ xs × y ≡ f x
+  ∈-map⁻ = Membershipₛ.∈-map⁻ (P.setoid A) (P.setoid B)
+
+  map-∈↔ : ∀ {y xs} → (∃ λ x → x ∈ xs × y ≡ f x) ↔ y ∈ map f xs
+  map-∈↔ {y} {xs} =
+    (∃ λ x → x ∈ xs × y ≡ f x)   ↔⟨ Any↔ ⟩
+    Any (λ x → y ≡ f x) xs       ↔⟨ map↔ ⟩
+    y ∈ List.map f xs            ∎
+    where open Related.EquationalReasoning
+
+------------------------------------------------------------------------
+-- _++_
+
+module _ {a} (A : Set a) {v : A} where
+
+  ∈-++⁺ˡ : ∀ {xs ys} → v ∈ xs → v ∈ xs ++ ys
+  ∈-++⁺ˡ = Membershipₛ.∈-++⁺ˡ (P.setoid A)
+
+  ∈-++⁺ʳ : ∀ xs {ys} → v ∈ ys → v ∈ xs ++ ys
+  ∈-++⁺ʳ = Membershipₛ.∈-++⁺ʳ (P.setoid A)
+
+  ∈-++⁻ : ∀ xs {ys} → v ∈ xs ++ ys → (v ∈ xs) ⊎ (v ∈ ys)
+  ∈-++⁻ = Membershipₛ.∈-++⁻ (P.setoid A)
+
+  ∈-insert : ∀ xs {ys} → v ∈ xs ++ [ v ] ++ ys
+  ∈-insert xs = Membershipₛ.∈-insert (P.setoid A) xs refl
+
+  ∈-∃++ : ∀ {xs} → v ∈ xs → ∃₂ λ ys zs → xs ≡ ys ++ [ v ] ++ zs
+  ∈-∃++ v∈xs with Membershipₛ.∈-∃++ (P.setoid A) v∈xs
+  ... | ys , zs , _ , refl , eq = ys , zs , ≋⇒≡ eq
+
+------------------------------------------------------------------------
+-- concat
+
+module _ {a} {A : Set a} {v : A} where
+
+  ∈-concat⁺ : ∀ {xss} → Any (v ∈_) xss → v ∈ concat xss
+  ∈-concat⁺ = Membershipₛ.∈-concat⁺ (P.setoid A)
+
+  ∈-concat⁻ : ∀ xss → v ∈ concat xss → Any (v ∈_) xss
+  ∈-concat⁻ = Membershipₛ.∈-concat⁻ (P.setoid A)
+
+  ∈-concat⁺′ : ∀ {vs xss} → v ∈ vs → vs ∈ xss → v ∈ concat xss
+  ∈-concat⁺′ v∈vs vs∈xss =
+    Membershipₛ.∈-concat⁺′ (P.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⁻′ (P.setoid A) xss v∈c
+  ... | xs , v∈xs , xs∈xss = xs , v∈xs , Any.map ≋⇒≡ xs∈xss
+
+  concat-∈↔ : ∀ {xss : List (List A)} →
+              (∃ λ xs → v ∈ xs × xs ∈ xss) ↔ v ∈ concat xss
+  concat-∈↔ {xss} =
+    (∃ λ xs → v ∈ xs × xs ∈ xss)  ↔⟨ Σ.cong Inv.id $ ×-comm _ _ ⟩
+    (∃ λ xs → xs ∈ xss × v ∈ xs)  ↔⟨ Any↔ ⟩
+    Any (Any (v ≡_)) xss          ↔⟨ concat↔ ⟩
+    v ∈ concat xss                ∎
+    where open Related.EquationalReasoning
+
+------------------------------------------------------------------------
+-- applyUpTo
+
+module _ {a} {A : Set a} where
+
+  ∈-applyUpTo⁺ : ∀ (f : ℕ → A) {i n} → i < n → f i ∈ applyUpTo f n
+  ∈-applyUpTo⁺ = Membershipₛ.∈-applyUpTo⁺ (P.setoid A)
+
+  ∈-applyUpTo⁻ : ∀ {v} f {n} → v ∈ applyUpTo f n →
+                 ∃ λ i → i < n × v ≡ f i
+  ∈-applyUpTo⁻ = Membershipₛ.∈-applyUpTo⁻ (P.setoid A)
+
+------------------------------------------------------------------------
+-- tabulate
+
+module _ {a} {A : Set a} where
+
+  ∈-tabulate⁺ : ∀ {n} {f : Fin n → A} i → f i ∈ tabulate f
+  ∈-tabulate⁺ = Membershipₛ.∈-tabulate⁺ (P.setoid A)
+
+  ∈-tabulate⁻ : ∀ {n} {f : Fin n → A} {v} →
+                v ∈ tabulate f → ∃ λ i → v ≡ f i
+  ∈-tabulate⁻ = Membershipₛ.∈-tabulate⁻ (P.setoid A)
+
+------------------------------------------------------------------------
+-- filter
+
+module _ {a p} {A : Set a} {P : A → Set p} (P? : Decidable P) where
+
+  ∈-filter⁺ : ∀ {x xs} → x ∈ xs → P x → x ∈ filter P? xs
+  ∈-filter⁺ = Membershipₛ.∈-filter⁺ (P.setoid A) P? (P.subst P)
+
+  ∈-filter⁻ : ∀ {v xs} → v ∈ filter P? xs → v ∈ xs × P v
+  ∈-filter⁻ = Membershipₛ.∈-filter⁻ (P.setoid A) P? (P.subst P)
+
+------------------------------------------------------------------------
+-- _>>=_
+
+module _ {ℓ} {A B : Set ℓ} where
+
+  >>=-∈↔ : ∀ {xs} {f : A → List B} {y} →
+           (∃ λ x → x ∈ xs × y ∈ f x) ↔ y ∈ (xs >>= f)
+  >>=-∈↔ {xs = xs} {f} {y} =
+    (∃ λ x → x ∈ xs × y ∈ f x)  ↔⟨ Any↔ ⟩
+    Any (Any (y ≡_) ∘ f) xs     ↔⟨ >>=↔ ⟩
+    y ∈ (xs >>= f)              ∎
+    where open Related.EquationalReasoning
+
+------------------------------------------------------------------------
+-- _⊛_
+
+module _ {ℓ} {A B : Set ℓ} where
+
+  ⊛-∈↔ : ∀ (fs : List (A → B)) {xs y} →
+         (∃₂ λ f x → f ∈ fs × x ∈ xs × y ≡ f x) ↔ y ∈ (fs ⊛ xs)
+  ⊛-∈↔ fs {xs} {y} =
+    (∃₂ λ f x → f ∈ fs × x ∈ xs × y ≡ f x)       ↔⟨ Σ.cong Inv.id (∃∃↔∃∃ _) ⟩
+    (∃ λ f → f ∈ fs × ∃ λ x → x ∈ xs × y ≡ f x)  ↔⟨ Σ.cong Inv.id ((_ ∎) ⟨ _×-cong_ ⟩ Any↔) ⟩
+    (∃ λ f → f ∈ fs × Any (_≡_ y ∘ f) xs)        ↔⟨ Any↔ ⟩
+    Any (λ f → Any (_≡_ y ∘ f) xs) fs            ↔⟨ ⊛↔ ⟩
+    y ∈ (fs ⊛ xs)                                ∎
+    where open Related.EquationalReasoning
+
+------------------------------------------------------------------------
+-- _⊗_
+
+module _ {ℓ} {A B : Set ℓ} where
+
+  ⊗-∈↔ : ∀ {xs ys} {x : A} {y : B} →
+         (x ∈ xs × y ∈ ys) ↔ (x , y) ∈ (xs ⊗ ys)
+  ⊗-∈↔ {xs} {ys} {x} {y} =
+    (x ∈ xs × y ∈ ys)             ↔⟨ ⊗↔′ ⟩
+    Any (x ≡_ ⟨×⟩ y ≡_) (xs ⊗ ys) ↔⟨ Any-cong ×-≡×≡↔≡,≡ (_ ∎) ⟩
+    (x , y) ∈ (xs ⊗ ys)           ∎
+    where
+    open Related.EquationalReasoning
+
+------------------------------------------------------------------------
+-- length
+
+module _ {a} {A : Set a} where
+
+  ∈-length : ∀ {x xs} → x ∈ xs → 1 ≤ length xs
+  ∈-length = Membershipₛ.∈-length (P.setoid A)
+
+------------------------------------------------------------------------
+-- lookup
+
+module _ {a} {A : Set a} where
+
+  ∈-lookup : ∀ xs i → lookup xs i ∈ xs
+  ∈-lookup = Membershipₛ.∈-lookup (P.setoid A)
+
+------------------------------------------------------------------------
+-- foldr
+
+module _ {a} {A : Set a} {_•_ : Op₂ A} where
+
+  foldr-selective : Selective _≡_ _•_ → ∀ e xs →
+                    (foldr _•_ e xs ≡ e) ⊎ (foldr _•_ e xs ∈ xs)
+  foldr-selective = Membershipₛ.foldr-selective (P.setoid A)
+
+------------------------------------------------------------------------
+-- Other properties
+
+-- Only a finite number of distinct elements can be members of a
+-- given list.
+
+module _ {a} {A : Set a} where
+
+  finite : (f : ℕ ↣ A) → ∀ xs → ¬ (∀ i → Injection.to f ⟨$⟩ i ∈ xs)
+  finite inj []       fᵢ∈[]   = ¬Any[] (fᵢ∈[] 0)
+  finite inj (x ∷ xs) fᵢ∈x∷xs = excluded-middle helper
+    where
+    open Injection inj renaming (injective to f-inj)
+
+    f : ℕ → A
+    f = to ⟨$⟩_
+
+    not-x : ∀ {i} → f i ≢ x → f i ∈ xs
+    not-x {i} fᵢ≢x with fᵢ∈x∷xs i
+    ... | here  fᵢ≡x  = contradiction fᵢ≡x fᵢ≢x
+    ... | there fᵢ∈xs = fᵢ∈xs
+
+    helper : ¬ Dec (∃ λ i → f i ≡ x)
+    helper (no fᵢ≢x)        = finite inj  xs (λ i → not-x (fᵢ≢x ∘ _,_ i))
+    helper (yes (i , fᵢ≡x)) = finite f′-inj xs f′ⱼ∈xs
+      where
+      f′ : ℕ → A
+      f′ j with i ≤? j
+      ... | yes i≤j = f (suc j)
+      ... | no  i≰j = 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 i≤j i≰1+j refl = i≰1+j (≤-step i≤j)
+
+      f′ⱼ∈xs : ∀ j → f′ j ∈ xs
+      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 {B = P.setoid A} (→-to-⟶ f′)
+      f′-injective′ {j} {k} eq with i ≤? j | i ≤? k
+      ... | yes _   | yes _   = P.cong pred (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  _   | no  _   = f-inj eq
+
+      f′-inj = record
+        { to        = →-to-⟶ f′
+        ; injective = f′-injective′
+        }
+
+------------------------------------------------------------------------
+-- DEPRECATED
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 0.15
+
+boolFilter-∈ : ∀ {a} {A : Set a} (p : A → Bool) (xs : List A) {x} →
+           x ∈ xs → p x ≡ true → x ∈ boolFilter p xs
+boolFilter-∈ p []       ()          _
+boolFilter-∈ p (x ∷ xs) (here refl) px≡true rewrite px≡true = here refl
+boolFilter-∈ p (y ∷ xs) (there pxs) px≡true with p y
+... | true  = there (boolFilter-∈ p xs pxs px≡true)
+... | false =        boolFilter-∈ p xs pxs px≡true
+{-# WARNING_ON_USAGE boolFilter-∈
+"Warning: boolFilter was deprecated in v0.15.
+Please use filter instead."
+#-}
+
+-- Version 0.16
+
+filter-∈ = ∈-filter⁺
+{-# WARNING_ON_USAGE filter-∈
+"Warning: filter-∈ was deprecated in v0.16.
+Please use ∈-filter⁺ instead."
+#-}
+
diff --git a/src/Data/List/Membership/Propositional/Properties/Core.agda b/src/Data/List/Membership/Propositional/Properties/Core.agda
new file mode 100644
index 0000000..a2129c5
--- /dev/null
+++ b/src/Data/List/Membership/Propositional/Properties/Core.agda
@@ -0,0 +1,74 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Core properties related to propositional list membership.
+--
+-- This file is needed to break the cyclic dependency with the proof
+-- `Any-cong` in `Data.Any.Properties` which relies on `Any↔` in this
+-- file.
+------------------------------------------------------------------------
+
+module Data.List.Membership.Propositional.Properties.Core where
+
+open import Function using (flip; id; _∘_)
+open import Function.Inverse using (_↔_; inverse)
+open import Data.List.Base using (List)
+open import Data.List.Any as Any using (Any; here; there)
+open import Data.List.Membership.Propositional
+open import Data.Product as Prod
+  using (_,_; proj₁; proj₂; uncurry′; ∃; _×_)
+open import Relation.Binary.PropositionalEquality as P
+  using (_≡_; refl)
+open import Relation.Unary using (_⊆_)
+
+-- Lemmas relating map and find.
+
+map∘find : ∀ {a p} {A : Set a} {P : A → Set 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 = P.cong here  hyp
+map∘find (there p) hyp = P.cong there (map∘find p hyp)
+
+find∘map : ∀ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q}
+           {xs : List A} (p : Any P xs) (f : P ⊆ Q) →
+           find (Any.map f p) ≡ Prod.map id (Prod.map id f) (find p)
+find∘map (here  p) f = refl
+find∘map (there p) f rewrite find∘map p f = refl
+
+-- find satisfies a simple equality when the predicate is a
+-- propositional equality.
+
+find-∈ : ∀ {a} {A : Set a} {x : A} {xs : List A} (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).
+
+lose∘find : ∀ {a p} {A : Set a} {P : A → Set p} {xs : List A}
+            (p : Any P xs) →
+            uncurry′ lose (proj₂ (find p)) ≡ p
+lose∘find p = map∘find p P.refl
+
+find∘lose : ∀ {a p} {A : Set a} (P : A → Set 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 (P.subst P) p)
+        | find-∈ x∈xs
+        = refl
+
+-- Any can be expressed using _∈_
+
+∃∈-Any : ∀ {a p} {A : Set a} {P : A → Set p} {xs} →
+         (∃ λ x → x ∈ xs × P x) → Any P xs
+∃∈-Any = uncurry′ lose ∘ proj₂
+
+Any↔ : ∀ {a p} {A : Set a} {P : A → Set p} {xs} →
+       (∃ λ x → x ∈ xs × P x) ↔ Any P xs
+Any↔ = inverse ∃∈-Any find from∘to lose∘find
+  where
+  from∘to : ∀ v → find (∃∈-Any v) ≡ v
+  from∘to p = find∘lose _ (proj₁ (proj₂ p)) (proj₂ (proj₂ p))
diff --git a/src/Data/List/Membership/Setoid.agda b/src/Data/List/Membership/Setoid.agda
new file mode 100644
index 0000000..a3384f1
--- /dev/null
+++ b/src/Data/List/Membership/Setoid.agda
@@ -0,0 +1,59 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- List membership and some related definitions
+------------------------------------------------------------------------
+
+open import Relation.Binary
+
+module Data.List.Membership.Setoid {c ℓ} (S : Setoid c ℓ) where
+
+open import Function using (_∘_; id; flip)
+open import Data.List.Base using (List; []; _∷_)
+open import Data.List.Any using (Any; map; here; there)
+open import Data.Product as Prod using (∃; _×_; _,_)
+open import Relation.Nullary using (¬_)
+
+open Setoid S renaming (Carrier to A)
+
+------------------------------------------------------------------------
+-- Definitions
+
+infix 4 _∈_ _∉_
+
+_∈_ : A → List A → Set _
+x ∈ xs = Any (x ≈_) xs
+
+_∉_ : A → List A → Set _
+x ∉ xs = ¬ x ∈ xs
+
+------------------------------------------------------------------------
+-- Operations
+
+mapWith∈ : ∀ {b} {B : Set b}
+           (xs : List A) → (∀ {x} → x ∈ xs → B) → List B
+mapWith∈ []       f = []
+mapWith∈ (x ∷ xs) f = f (here refl) ∷ mapWith∈ xs (f ∘ there)
+
+find : ∀ {p} {P : A → Set p} {xs} →
+       Any P xs → ∃ λ x → x ∈ xs × P x
+find (here px)   = (_ , here refl , px)
+find (there pxs) = Prod.map id (Prod.map there id) (find pxs)
+
+lose : ∀ {p} {P : A → Set p} {x xs} →
+       P Respects _≈_ → x ∈ xs → P x → Any P xs
+lose resp x∈xs px = map (flip resp px) x∈xs
+
+------------------------------------------------------------------------
+-- DEPRECATED
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 0.16
+
+map-with-∈ = mapWith∈
+{-# WARNING_ON_USAGE map-with-∈
+"Warning: map-with-∈ was deprecated in v0.16.
+Please use mapWith∈ instead."
+#-}
diff --git a/src/Data/List/Membership/Setoid/Properties.agda b/src/Data/List/Membership/Setoid/Properties.agda
new file mode 100644
index 0000000..a8f3a97
--- /dev/null
+++ b/src/Data/List/Membership/Setoid/Properties.agda
@@ -0,0 +1,239 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties related to setoid list membership
+------------------------------------------------------------------------
+
+module Data.List.Membership.Setoid.Properties where
+
+open import Algebra.FunctionProperties using (Op₂; Selective)
+open import Data.Fin using (Fin; zero; suc)
+open import Data.List
+open import Data.List.Any as Any using (Any; here; there)
+import Data.List.Any.Properties as Any
+import Data.List.Membership.Setoid as Membership
+import Data.List.Relation.Equality.Setoid as Equality
+open import Data.Nat using (z≤n; s≤s; _≤_; _<_)
+open import Data.Nat.Properties using (≤-trans; n≤1+n)
+open import Data.Product as Prod using (∃; _×_; _,_ ; ∃₂)
+open import Data.Sum using (_⊎_; inj₁; inj₂)
+open import Function using (flip; _∘_; id)
+open import Relation.Binary hiding (Decidable)
+open import Relation.Unary using (Decidable; Pred)
+open import Relation.Nullary using (yes; no)
+open import Relation.Nullary.Negation using (contradiction)
+open Setoid using (Carrier)
+
+------------------------------------------------------------------------
+-- Equality properties
+
+module _ {c ℓ} (S : Setoid c ℓ) where
+
+  open Setoid S
+  open Equality S
+  open Membership S
+
+  -- _∈_ respects the underlying equality
+
+  ∈-resp-≈ : ∀ {xs} → (_∈ xs) Respects _≈_
+  ∈-resp-≈ x≈y x∈xs = Any.map (trans (sym x≈y)) x∈xs
+
+  ∉-resp-≈ : ∀ {xs} → (_∉ xs) Respects _≈_
+  ∉-resp-≈ v≈w v∉xs w∈xs = v∉xs (∈-resp-≈ (sym v≈w) w∈xs)
+
+  ∈-resp-≋ : ∀ {x} → (x ∈_) Respects _≋_
+  ∈-resp-≋ = Any.lift-resp (flip trans)
+
+  ∉-resp-≋ : ∀ {x} → (x ∉_) Respects _≋_
+  ∉-resp-≋ xs≋ys v∉xs v∈ys = v∉xs (∈-resp-≋ (≋-sym xs≋ys) v∈ys)
+
+------------------------------------------------------------------------
+-- mapWith∈
+
+module _ {c₁ c₂ ℓ₁ ℓ₂} (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 _≈₂_; refl to refl₂)
+  open Equality S₁ using ([]; _∷_) renaming (_≋_ to _≋₁_)
+  open Equality S₂ using () renaming (_≋_ to _≋₂_)
+  open Membership S₁
+
+  mapWith∈-cong : ∀ {xs ys} → xs ≋₁ ys →
+                  (f : ∀ {x} → x ∈ xs → A₂) →
+                  (g : ∀ {y} → y ∈ ys → A₂) →
+                  (∀ {x y} → x ≈₁ y → (x∈xs : x ∈ xs) (y∈ys : y ∈ ys) →
+                     f x∈xs ≈₂ g y∈ys) →
+                  mapWith∈ xs f ≋₂ mapWith∈ ys g
+  mapWith∈-cong []            f g cong = []
+  mapWith∈-cong (x≈y ∷ xs≋ys) f g cong =
+    cong x≈y (here refl₁) (here refl₁) ∷
+    mapWith∈-cong xs≋ys (f ∘ there) (g ∘ there)
+      (λ x≈y x∈xs y∈ys → cong x≈y (there x∈xs) (there y∈ys))
+
+  mapWith∈≗map : ∀ f xs → mapWith∈ xs (λ {x} _ → f x) ≋₂ map f xs
+  mapWith∈≗map f []       = []
+  mapWith∈≗map f (x ∷ xs) = refl₂ ∷ mapWith∈≗map f xs
+
+------------------------------------------------------------------------
+-- map
+
+module _ {c₁ c₂ ℓ₁ ℓ₂} (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 Membership S₁ using (find) renaming (_∈_ to _∈₁_)
+  open Membership S₂ using () renaming (_∈_ to _∈₂_)
+
+  ∈-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)
+
+------------------------------------------------------------------------
+-- _++_
+
+module _ {c ℓ} (S : Setoid c ℓ) where
+
+  open Membership S using (_∈_)
+  open Setoid S
+  open Equality S using (_≋_; _∷_; ≋-refl)
+
+  ∈-++⁺ˡ : ∀ {v xs ys} → v ∈ xs → v ∈ xs ++ ys
+  ∈-++⁺ˡ = Any.++⁺ˡ
+
+  ∈-++⁺ʳ : ∀ {v} xs {ys} → v ∈ ys → v ∈ xs ++ ys
+  ∈-++⁺ʳ = Any.++⁺ʳ
+
+  ∈-++⁻ : ∀ {v} xs {ys} → v ∈ xs ++ ys → (v ∈ xs) ⊎ (v ∈ ys)
+  ∈-++⁻ = Any.++⁻
+
+  ∈-insert : ∀ xs {ys v w} → v ≈ w → v ∈ xs ++ [ w ] ++ ys
+  ∈-insert xs = Any.++-insert xs
+
+  ∈-∃++ : ∀ {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
+
+------------------------------------------------------------------------
+-- concat
+
+module _ {c ℓ} (S : Setoid c ℓ) where
+
+  open Setoid S using (_≈_)
+  open Membership S using (_∈_)
+  open Equality S using (≋-setoid)
+  open Membership ≋-setoid using (find) renaming (_∈_ to _∈ₗ_)
+
+  ∈-concat⁺ : ∀ {v xss} → Any (v ∈_) xss → v ∈ concat xss
+  ∈-concat⁺ = Any.concat⁺
+
+  ∈-concat⁻ : ∀ {v} xss → v ∈ concat xss → Any (v ∈_) xss
+  ∈-concat⁻ = Any.concat⁻
+
+  ∈-concat⁺′ : ∀ {v vs xss} → v ∈ vs → vs ∈ₗ xss → v ∈ concat xss
+  ∈-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
+
+------------------------------------------------------------------------
+-- applyUpTo
+
+module _ {c ℓ} (S : Setoid c ℓ) where
+
+  open Setoid S using (_≈_; refl)
+  open Membership S using (_∈_)
+
+  ∈-applyUpTo⁺ : ∀ f {i n} → i < n → f i ∈ applyUpTo f n
+  ∈-applyUpTo⁺ f = Any.applyUpTo⁺ f refl
+
+  ∈-applyUpTo⁻ : ∀ {v} f {n} → v ∈ applyUpTo f n →
+                 ∃ λ i → i < n × v ≈ f i
+  ∈-applyUpTo⁻ = Any.applyUpTo⁻
+
+------------------------------------------------------------------------
+-- tabulate
+
+module _ {c ℓ} (S : Setoid c ℓ) where
+
+  open Setoid S using (_≈_; refl) renaming (Carrier to A)
+  open Membership S using (_∈_)
+
+  ∈-tabulate⁺ : ∀ {n} {f : Fin n → A} i → f i ∈ tabulate f
+  ∈-tabulate⁺ i = Any.tabulate⁺ i refl
+
+  ∈-tabulate⁻ : ∀ {n} {f : Fin n → A} {v} →
+                v ∈ tabulate f → ∃ λ i → v ≈ f i
+  ∈-tabulate⁻ = Any.tabulate⁻
+
+------------------------------------------------------------------------
+-- filter
+
+module _ {c ℓ p} (S : Setoid c ℓ) {P : Pred (Carrier S) p}
+         (P? : Decidable P) (resp : P Respects (Setoid._≈_ S)) where
+
+  open Setoid S using (_≈_; sym)
+  open Membership S using (_∈_)
+
+  ∈-filter⁺ : ∀ {v xs} → v ∈ xs → P v → v ∈ filter P? xs
+  ∈-filter⁺ {xs = x ∷ _} (here v≈x) Pv with P? x
+  ... | yes _   = here v≈x
+  ... | no  ¬Px = contradiction (resp v≈x Pv) ¬Px
+  ∈-filter⁺ {xs = x ∷ _} (there v∈xs) Pv with P? x
+  ... | yes _ = there (∈-filter⁺ v∈xs Pv)
+  ... | no  _ = ∈-filter⁺ v∈xs Pv
+
+  ∈-filter⁻ : ∀ {v xs} → v ∈ filter P? xs → v ∈ xs × P v
+  ∈-filter⁻ {xs = []}     ()
+  ∈-filter⁻ {xs = x ∷ xs} v∈f[x∷xs] with P? x
+  ... | no  _  = Prod.map there id (∈-filter⁻ v∈f[x∷xs])
+  ... | yes Px with v∈f[x∷xs]
+  ...   | here  v≈x   = here v≈x , resp (sym v≈x) Px
+  ...   | there v∈fxs = Prod.map there id (∈-filter⁻ v∈fxs)
+
+------------------------------------------------------------------------
+-- length
+
+module _ {c ℓ} (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 _)
+
+------------------------------------------------------------------------
+-- lookup
+
+module _ {c ℓ} (S : Setoid c ℓ) where
+
+  open Setoid S using (refl)
+  open Membership S using (_∈_)
+
+  ∈-lookup : ∀ xs i → lookup xs i ∈ xs
+  ∈-lookup []       ()
+  ∈-lookup (x ∷ xs) zero    = here refl
+  ∈-lookup (x ∷ xs) (suc i) = there (∈-lookup xs i)
+
+------------------------------------------------------------------------
+-- foldr
+
+module _ {c ℓ} (S : Setoid c ℓ) {_•_ : Op₂ (Carrier S)} where
+
+  open Setoid S using (_≈_; refl; sym; trans)
+  open Membership S using (_∈_)
+
+  foldr-selective : Selective _≈_ _•_ → ∀ e xs →
+                    (foldr _•_ e xs ≈ e) ⊎ (foldr _•_ e xs ∈ xs)
+  foldr-selective •-sel i [] = inj₁ refl
+  foldr-selective •-sel i (x ∷ xs) with •-sel x (foldr _•_ i xs)
+  ... | inj₁ x•f≈x = inj₂ (here x•f≈x)
+  ... | inj₂ x•f≈f with foldr-selective •-sel i xs
+  ...   | inj₁ f≈i  = inj₁ (trans x•f≈f f≈i)
+  ...   | inj₂ f∈xs = inj₂ (∈-resp-≈ S (sym x•f≈f) (there f∈xs))