```------------------------------------------------------------------------
-- The Agda standard library
--
-- Any predicate transformer for fresh lists
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Data.List.Fresh.Relation.Unary.Any where

open import Level using (Level; _⊔_; Lift)
open import Data.Empty
open import Data.Product using (∃; _,_; -,_)
open import Data.Sum.Base using (_⊎_; [_,_]′; inj₁; inj₂)
open import Function.Bundles using (_⇔_; mk⇔)
open import Relation.Nullary.Negation using (¬_)
open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _⊎-dec_)
open import Relation.Unary  as U
open import Relation.Binary as B using (Rel)

open import Data.List.Fresh using (List#; []; cons; _∷#_; _#_)

private
variable
a p q r : Level
A : Set a

module _ {A : Set a} {R : Rel A r} (P : Pred A p) where

data Any : List# A R → Set (p ⊔ a ⊔ r) where
here  : ∀ {x xs pr} → P x → Any (cons x xs pr)
there : ∀ {x xs pr} → Any xs → Any (cons x xs pr)

module _ {R : Rel A r} {P : Pred A p} {x} {xs : List# A R} {pr} where

head : ¬ Any P xs → Any P (cons x xs pr) → P x
head ¬tail (here p)   = p
head ¬tail (there ps) = ⊥-elim (¬tail ps)

tail : ¬ P x → Any P (cons x xs pr) → Any P xs
tail ¬head (there ps) = ps

toSum : Any P (cons x xs pr) → P x ⊎ Any P xs
toSum (here p) = inj₁ p
toSum (there ps) = inj₂ ps

fromSum : P x ⊎ Any P xs → Any P (cons x xs pr)
fromSum = [ here , there ]′

⊎⇔Any : (P x ⊎ Any P xs) ⇔ Any P (cons x xs pr)
⊎⇔Any = mk⇔ fromSum toSum

module _ {R : Rel A r} {P : Pred A p} {Q : Pred A q} where

map : {xs : List# A R} → ∀[ P ⇒ Q ] → Any P xs → Any Q xs
map p⇒q (here p)  = here (p⇒q p)
map p⇒q (there p) = there (map p⇒q p)

module _ {R : Rel A r} {P : Pred A p} where

witness : {xs : List# A R} → Any P xs → ∃ P
witness (here p)   = -, p
witness (there ps) = witness ps

remove   : (xs : List# A R) → Any P xs → List# A R
remove-# : ∀ {x} {xs : List# A R} p → x # xs → x # (remove xs p)

remove (_ ∷# xs)      (here _)  = xs
remove (cons x xs pr) (there k) = cons x (remove xs k) (remove-# k pr)

remove-# (here x)  (p , ps) = ps
remove-# (there k) (p , ps) = p , remove-# k ps

infixl 4 _─_
_─_ = remove

module _ {R : Rel A r} {P : Pred A p} (P? : Decidable P) where

any? : (xs : List# A R) → Dec (Any P xs)
any? []        = no (λ ())
any? (x ∷# xs) = Dec.map ⊎⇔Any (P? x ⊎-dec any? xs)
```