Add All.lookup over setoid membership (#1337)

Author: lexvanderstoep

src/Data/List/Relation/Unary/All.agda

@@ -207,6 +207,13 @@ module _ {P : Pred A p} where
   lookup : ∀ {xs} → 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ₛ : ∀ {xs} → P Respects _≈_ → All P xs → (∀ {x} → x ∈ xs → P x)
+  lookupₛ resp pxs = lookupWith (λ py x=y → resp (sym₁ x=y) py) pxs
+
 ------------------------------------------------------------------------
 -- Properties of predicates preserved by All