```------------------------------------------------------------------------
-- 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.

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

module Data.List.Membership.Propositional.Properties.Core where

open import Function.Base using (flip; id; _∘_)
open import Function.Inverse using (_↔_; inverse)
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 as Prod
using (_,_; proj₁; proj₂; uncurry′; ∃; _×_)
open import Level using (Level)
open import Relation.Binary.PropositionalEquality as P
using (_≡_; refl)
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 = P.cong here  hyp
map∘find (there p) hyp = P.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) ≡ 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-∈ : ∀ {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 : ∀ {P : Pred A p} {xs : List A}
(p : Any P xs) →
uncurry′ lose (proj₂ (find p)) ≡ p
lose∘find p = map∘find p P.refl

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 (P.subst P) p)
| find-∈ x∈xs
= 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↔ : ∀ {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))
```