    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- AVL trees where at least one element satisfies a given property
    ------------------------------------------------------------------------

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

    open import Relation.Binary.Bundles using (StrictTotalOrder)

    module Data.Tree.AVL.Relation.Unary.Any
      {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
      where

    open import Data.Product.Base as Product using (∃)
    open import Function.Base using (_∘_; _$_)
    open import Level using (Level; _⊔_)

    open import Relation.Nullary.Decidable using (map′)
    open import Relation.Unary

    open StrictTotalOrder strictTotalOrder renaming (Carrier to Key)
    open import Data.Tree.AVL.Indexed strictTotalOrder as Indexed using (K&_; _,_)
    open import Data.Tree.AVL strictTotalOrder using (Tree; tree; Value)
    import Data.Tree.AVL.Indexed.Relation.Unary.Any strictTotalOrder as AVLₚ

    private
      variable
        v p q : Level
        V : Value v
        t : Tree V
        P : Pred (K& V) p
        Q : Pred (K& V) q

    ------------------------------------------------------------------------
    -- Definition

    -- Given a predicate P, Any P t describes a path in t to an element that
    -- satisfies P. There may be others.
    -- See `Relation.Unary` for an explanation of predicates.

    data Any {V : Value v} (P : Pred (K& V) p) :
             Tree V → Set (p ⊔ a ⊔ v ⊔ ℓ₂) where
      tree : ∀ {h t} → AVLₚ.Any P t → Any P (tree {h = h} t)

    ------------------------------------------------------------------------
    -- Operations on Any

    map : P ⊆ Q → Any P t → Any Q t
    map f (tree p) = tree (AVLₚ.map f p)

    lookup : Any {V = V} P t → K& V
    lookup (tree p) = AVLₚ.lookup p

    lookupKey : Any P t → Key
    lookupKey (tree p) = AVLₚ.lookupKey p

    -- If any element satisfies P, then P is satisfied.

    satisfied : Any P t → ∃ P
    satisfied (tree p) = AVLₚ.satisfied p

    ------------------------------------------------------------------------
    -- Properties of predicates preserved by Any

    any? : Decidable P → Decidable (Any {V = V} P)
    any? P? (tree p) = map′ tree (λ where (tree p) → p) (AVLₚ.any? P? p)

    satisfiable : (k : Key) → Satisfiable (P ∘ (k ,_)) → Satisfiable (Any {V = V} P)
    satisfiable k sat = Product.map tree tree
                      $ AVLₚ.satisfiable Indexed.⊥⁺<[ k ] Indexed.[ k ]<⊤⁺ sat